Data flow: Earlier call-context based dispatch filtering

This commit is contained in:
Tom Hvitved
2023-08-16 12:05:10 +02:00
parent 44b734e120
commit 570654d1f0
2 changed files with 199 additions and 104 deletions

View File

@@ -1145,11 +1145,21 @@ module MakeImpl<InputSig Lang> {
class LocalCc;
bindingset[call, c, outercc]
CcCall getCallContextCall(DataFlowCall call, DataFlowCallable c, Cc outercc);
DataFlowCallable viableImplCallContextReduced(DataFlowCall call, CcCall ctx);
bindingset[call, c, innercc]
CcNoCall getCallContextReturn(DataFlowCallable c, DataFlowCall call, Cc innercc);
bindingset[call, ctx]
predicate viableImplNotCallContextReduced(DataFlowCall call, Cc ctx);
bindingset[call, c]
CcCall getCallContextCall(DataFlowCall call, DataFlowCallable c);
DataFlowCallable viableImplCallContextReducedReverse(DataFlowCall call, CcNoCall ctx);
bindingset[ctx]
predicate viableImplNotCallContextReducedReverse(CcNoCall ctx);
bindingset[call, c]
CcNoCall getCallContextReturn(DataFlowCallable c, DataFlowCall call);
bindingset[node, cc]
LocalCc getLocalCc(NodeEx node, Cc cc);
@@ -1191,21 +1201,24 @@ module MakeImpl<InputSig Lang> {
pragma[nomagic]
private predicate flowIntoCallApa(
DataFlowCall call, ArgNodeEx arg, ParamNodeEx p, boolean allowsFieldFlow, ApApprox apa
DataFlowCall call, ArgNodeEx arg, ParamNodeEx p, DataFlowCallable c,
boolean allowsFieldFlow, ApApprox apa
) {
flowIntoCall(call, arg, p, allowsFieldFlow) and
PrevStage::revFlowAp(p, pragma[only_bind_into](apa)) and
PrevStage::revFlowAp(arg, pragma[only_bind_into](apa))
PrevStage::revFlowAp(arg, pragma[only_bind_into](apa)) and
c = p.getEnclosingCallable()
}
pragma[nomagic]
private predicate flowOutOfCallApa(
DataFlowCall call, RetNodeEx ret, ReturnKindExt kind, NodeEx out, boolean allowsFieldFlow,
ApApprox apa
DataFlowCall call, RetNodeEx ret, DataFlowCallable c, ReturnKindExt kind, NodeEx out,
boolean allowsFieldFlow, ApApprox apa
) {
flowOutOfCall(call, ret, kind, out, allowsFieldFlow) and
PrevStage::revFlowAp(out, pragma[only_bind_into](apa)) and
PrevStage::revFlowAp(ret, pragma[only_bind_into](apa))
PrevStage::revFlowAp(ret, pragma[only_bind_into](apa)) and
c = ret.getEnclosingCallable()
}
pragma[nomagic]
@@ -1214,7 +1227,7 @@ module MakeImpl<InputSig Lang> {
ApApprox argApa, ApApprox apa
) {
exists(ReturnKindExt kind |
flowOutOfCallApa(call, ret, kind, out, allowsFieldFlow, apa) and
flowOutOfCallApa(call, ret, _, kind, out, allowsFieldFlow, apa) and
PrevStage::callMayFlowThroughRev(call) and
PrevStage::returnMayFlowThrough(ret, argApa, apa, kind) and
matchesCall(ccc, call)
@@ -1332,16 +1345,7 @@ module MakeImpl<InputSig Lang> {
)
or
// flow out of a callable
exists(
DataFlowCall call, RetNodeEx ret, boolean allowsFieldFlow, CcNoCall innercc,
DataFlowCallable inner
|
fwdFlow(ret, state, innercc, summaryCtx, argT, argAp, t, ap, apa) and
flowOutOfCallApa(call, ret, _, node, allowsFieldFlow, apa) and
inner = ret.getEnclosingCallable() and
cc = getCallContextReturn(inner, call, innercc) and
if allowsFieldFlow = false then ap instanceof ApNil else any()
)
fwdFlowOut(node, state, cc, summaryCtx, argT, argAp, t, ap, apa)
or
// flow through a callable
exists(
@@ -1408,15 +1412,98 @@ module MakeImpl<InputSig Lang> {
)
}
pragma[nomagic]
private predicate fwdFlowIn0(
DataFlowCall call, ArgNodeEx arg, FlowState state, Cc outercc, ParamNodeOption summaryCtx,
TypOption argT, ApOption argAp, Typ t, Ap ap, ApApprox apa
) {
fwdFlow(arg, state, outercc, summaryCtx, argT, argAp, t, ap, apa) and
flowIntoCallApa(call, arg, _, _, _, _)
}
pragma[nomagic]
private predicate fwdFlowInCallContextReduced(
DataFlowCall call, ArgNodeEx arg, FlowState state, CcCall outercc,
ParamNodeOption summaryCtx, TypOption argT, ApOption argAp, Typ t, Ap ap, ApApprox apa,
DataFlowCallable inner
) {
fwdFlowIn0(call, arg, state, outercc, summaryCtx, argT, argAp, t, ap, apa) and
inner = viableImplCallContextReduced(call, outercc)
}
pragma[nomagic]
private predicate fwdFlowInNotCallContextReduced(
DataFlowCall call, ArgNodeEx arg, FlowState state, Cc outercc, ParamNodeOption summaryCtx,
TypOption argT, ApOption argAp, Typ t, Ap ap, ApApprox apa
) {
fwdFlowIn0(call, arg, state, outercc, summaryCtx, argT, argAp, t, ap, apa) and
viableImplNotCallContextReduced(call, outercc)
}
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(ArgNodeEx arg, boolean allowsFieldFlow |
fwdFlow(arg, state, outercc, summaryCtx, argT, argAp, t, ap, apa) and
flowIntoCallApa(call, arg, p, allowsFieldFlow, apa) and
innercc = getCallContextCall(call, p.getEnclosingCallable(), outercc) and
exists(ArgNodeEx arg, boolean allowsFieldFlow, DataFlowCallable inner |
fwdFlowInCallContextReduced(call, arg, state, outercc, summaryCtx, argT, argAp, t, ap,
apa, inner)
or
fwdFlowInNotCallContextReduced(call, arg, state, outercc, summaryCtx, argT, argAp, t,
ap, apa)
|
flowIntoCallApa(call, arg, p, inner, allowsFieldFlow, apa) and
innercc = getCallContextCall(call, inner) and
if allowsFieldFlow = false then ap instanceof ApNil else any()
)
}
pragma[nomagic]
private predicate fwdFlowOut0(
RetNodeEx ret, FlowState state, CcNoCall innercc, ParamNodeOption summaryCtx,
TypOption argT, ApOption argAp, Typ t, Ap ap, ApApprox apa, DataFlowCallable inner
) {
fwdFlow(ret, state, innercc, summaryCtx, argT, argAp, t, ap, apa) and
inner = ret.getEnclosingCallable()
}
pragma[nomagic]
private predicate fwdFlowOutCallContextReduced(
DataFlowCall call, RetNodeEx ret, FlowState state, CcNoCall innercc,
ParamNodeOption summaryCtx, TypOption argT, ApOption argAp, Typ t, Ap ap, ApApprox apa,
DataFlowCallable inner
) {
fwdFlowOut0(ret, state, innercc, summaryCtx, argT, argAp, t, ap, apa, inner) and
inner = viableImplCallContextReducedReverse(call, innercc)
}
pragma[nomagic]
private predicate fwdFlowOutNotCallContextReduced(
RetNodeEx ret, FlowState state, CcNoCall innercc, ParamNodeOption summaryCtx,
TypOption argT, ApOption argAp, Typ t, Ap ap, ApApprox apa, DataFlowCallable inner
) {
fwdFlowOut0(ret, state, innercc, summaryCtx, argT, argAp, t, ap, apa, inner) and
viableImplNotCallContextReducedReverse(innercc)
}
// 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
) {
exists(
DataFlowCall call, RetNodeEx ret, boolean allowsFieldFlow, CcNoCall innercc,
DataFlowCallable inner
|
fwdFlowOutCallContextReduced(call, ret, state, innercc, summaryCtx, argT, argAp, t, ap,
apa, inner)
or
fwdFlowOutNotCallContextReduced(ret, state, innercc, summaryCtx, argT, argAp, t, ap,
apa, inner)
|
flowOutOfCallApa(call, ret, inner, _, out, allowsFieldFlow, apa) and
outercc = getCallContextReturn(inner, call) and
if allowsFieldFlow = false then ap instanceof ApNil else any()
)
}
@@ -1518,7 +1605,7 @@ module MakeImpl<InputSig Lang> {
DataFlowCall call, ArgNodeEx arg, ParamNodeEx p, boolean allowsFieldFlow, Ap argAp, Ap ap
) {
exists(ApApprox argApa, Typ argT |
flowIntoCallApa(call, pragma[only_bind_into](arg), pragma[only_bind_into](p),
flowIntoCallApa(call, pragma[only_bind_into](arg), pragma[only_bind_into](p), _,
allowsFieldFlow, argApa) and
fwdFlow(arg, _, _, _, _, _, pragma[only_bind_into](argT), pragma[only_bind_into](argAp),
argApa) and
@@ -1529,24 +1616,23 @@ module MakeImpl<InputSig Lang> {
}
pragma[nomagic]
private predicate flowIntoCallAp(
DataFlowCall call, ArgNodeEx arg, ParamNodeEx p, boolean allowsFieldFlow, Ap ap
) {
exists(ApApprox apa |
flowIntoCallApa(call, arg, p, allowsFieldFlow, apa) and
fwdFlow(arg, _, _, _, _, _, _, ap, apa)
private predicate flowIntoCallAp(DataFlowCall call, ArgNodeEx arg, ParamNodeEx p, Ap ap) {
exists(ApApprox apa, boolean allowsFieldFlow |
flowIntoCallApa(call, arg, p, _, allowsFieldFlow, apa) and
fwdFlow(arg, _, _, _, _, _, _, ap, apa) and
if allowsFieldFlow = false then ap instanceof ApNil else any()
)
}
pragma[nomagic]
private predicate flowOutOfCallAp(
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, NodeEx out, boolean allowsFieldFlow,
Ap ap
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, NodeEx out, Ap ap
) {
exists(ApApprox apa |
flowOutOfCallApa(call, ret, _, out, allowsFieldFlow, apa) and
exists(ApApprox apa, boolean allowsFieldFlow |
flowOutOfCallApa(call, ret, _, _, out, allowsFieldFlow, apa) and
fwdFlow(ret, _, _, _, _, _, _, ap, apa) and
pos = ret.getReturnPosition()
pos = ret.getReturnPosition() and
if allowsFieldFlow = false then ap instanceof ApNil else any()
)
}
@@ -1627,10 +1713,9 @@ module MakeImpl<InputSig Lang> {
)
or
// flow into a callable
exists(ParamNodeEx p, boolean allowsFieldFlow |
exists(ParamNodeEx p |
revFlow(p, state, TReturnCtxNone(), returnAp, ap) and
flowIntoCallAp(_, node, p, allowsFieldFlow, ap) and
(if allowsFieldFlow = false then ap instanceof ApNil else any()) and
flowIntoCallAp(_, node, p, ap) and
returnCtx = TReturnCtxNone()
)
or
@@ -1680,10 +1765,9 @@ module MakeImpl<InputSig Lang> {
DataFlowCall call, RetNodeEx ret, ReturnPosition pos, FlowState state,
ReturnCtx returnCtx, ApOption returnAp, Ap ap
) {
exists(NodeEx out, boolean allowsFieldFlow |
exists(NodeEx out |
revFlow(out, state, returnCtx, returnAp, ap) and
flowOutOfCallAp(call, ret, pos, out, allowsFieldFlow, ap) and
if allowsFieldFlow = false then ap instanceof ApNil else any()
flowOutOfCallAp(call, ret, pos, out, ap)
)
}
@@ -1872,11 +1956,23 @@ module MakeImpl<InputSig Lang> {
bindingset[node, cc]
LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
bindingset[call, c, outercc]
CcCall getCallContextCall(DataFlowCall call, DataFlowCallable c, Cc outercc) { any() }
DataFlowCallable viableImplCallContextReduced(DataFlowCall call, CcCall ctx) { none() }
bindingset[call, c, innercc]
CcNoCall getCallContextReturn(DataFlowCallable c, DataFlowCall call, Cc innercc) { any() }
bindingset[call, ctx]
predicate viableImplNotCallContextReduced(DataFlowCall call, Cc ctx) { any() }
bindingset[call, c]
CcCall getCallContextCall(DataFlowCall call, DataFlowCallable c) { any() }
DataFlowCallable viableImplCallContextReducedReverse(DataFlowCall call, CcNoCall ctx) {
none()
}
bindingset[ctx]
predicate viableImplNotCallContextReducedReverse(CcNoCall ctx) { any() }
bindingset[call, c]
CcNoCall getCallContextReturn(DataFlowCallable c, DataFlowCall call) { any() }
}
private module Level1CallContext {
@@ -1899,9 +1995,17 @@ module MakeImpl<InputSig Lang> {
bindingset[node, cc]
LocalCc getLocalCc(NodeEx node, Cc cc) { any() }
bindingset[call, c, outercc]
CcCall getCallContextCall(DataFlowCall call, DataFlowCallable c, Cc outercc) {
checkCallContextCall(outercc, call, c) and
DataFlowCallable viableImplCallContextReduced(DataFlowCall call, CcCall ctx) {
result = prunedViableImplInCallContext(call, ctx)
}
bindingset[call, ctx]
predicate viableImplNotCallContextReduced(DataFlowCall call, Cc ctx) {
noPrunedViableImplInCallContext(call, ctx)
}
bindingset[call, c]
CcCall getCallContextCall(DataFlowCall call, DataFlowCallable c) {
if recordDataFlowCallSiteDispatch(call, c)
then result = TSpecificCall(call)
else result = TSomeCall()
@@ -1918,18 +2022,34 @@ module MakeImpl<InputSig Lang> {
node.getEnclosingCallable())
}
bindingset[call, c, outercc]
CcCall getCallContextCall(DataFlowCall call, DataFlowCallable c, Cc outercc) {
checkCallContextCall(outercc, call, c) and
DataFlowCallable viableImplCallContextReduced(DataFlowCall call, CcCall ctx) {
result = prunedViableImplInCallContext(call, ctx)
}
bindingset[call, ctx]
predicate viableImplNotCallContextReduced(DataFlowCall call, Cc ctx) {
noPrunedViableImplInCallContext(call, ctx)
}
bindingset[call, c]
CcCall getCallContextCall(DataFlowCall call, DataFlowCallable c) {
if recordDataFlowCallSite(call, c)
then result = TSpecificCall(call)
else result = TSomeCall()
}
}
bindingset[call, c, innercc]
CcNoCall getCallContextReturn(DataFlowCallable c, DataFlowCall call, Cc innercc) {
checkCallContextReturn(innercc, c, call) and
DataFlowCallable viableImplCallContextReducedReverse(DataFlowCall call, CcNoCall ctx) {
result = prunedViableImplInCallContextReverse(call, ctx)
}
bindingset[ctx]
predicate viableImplNotCallContextReducedReverse(CcNoCall ctx) {
ctx instanceof CallContextAny
}
bindingset[call, c]
CcNoCall getCallContextReturn(DataFlowCallable c, DataFlowCall call) {
if reducedViableImplInReturn(c, call) then result = TReturn(c, call) else result = ccNone()
}
}

View File

@@ -750,9 +750,11 @@ module MakeImplCommon<InputSig Lang> {
* makes a difference.
*/
cached
DataFlowCallable prunedViableImplInCallContext(DataFlowCall call, DataFlowCall ctx) {
result = viableImplInCallContextExt(call, ctx) and
reducedViableImplInCallContext(call, _, ctx)
DataFlowCallable prunedViableImplInCallContext(DataFlowCall call, CallContextSpecificCall ctx) {
exists(DataFlowCall outer | ctx = TSpecificCall(outer) |
result = viableImplInCallContextExt(call, outer) and
reducedViableImplInCallContext(call, _, outer)
)
}
/**
@@ -778,9 +780,13 @@ module MakeImplCommon<InputSig Lang> {
* `ctx`.
*/
cached
DataFlowCallable prunedViableImplInCallContextReverse(DataFlowCall call, DataFlowCall ctx) {
result = viableImplInCallContextExt(call, ctx) and
reducedViableImplInReturn(result, call)
DataFlowCallable prunedViableImplInCallContextReverse(DataFlowCall call, CallContextReturn ctx) {
exists(DataFlowCallable c0, DataFlowCall call0 |
callEnclosingCallable(call0, result) and
ctx = TReturn(c0, call0) and
c0 = viableImplInCallContextExt(call0, call) and
reducedViableImplInReturn(c0, call0)
)
}
}
@@ -1278,38 +1284,18 @@ module MakeImplCommon<InputSig Lang> {
result = getReturnPosition0(ret, ret.getKind())
}
/**
* Checks whether `inner` can return to `call` in the call context `innercc`.
* Assumes a context of `inner = viableCallableExt(call)`.
*/
bindingset[innercc, inner, call]
predicate checkCallContextReturn(CallContext innercc, DataFlowCallable inner, DataFlowCall call) {
innercc instanceof CallContextAny
or
exists(DataFlowCallable c0, DataFlowCall call0 |
callEnclosingCallable(call0, inner) and
innercc = TReturn(c0, call0) and
c0 = prunedViableImplInCallContextReverse(call0, call)
)
}
/**
* Checks whether `call` can resolve to `calltarget` in the call context `cc`.
* Assumes a context of `calltarget = viableCallableExt(call)`.
*/
bindingset[cc, call, calltarget]
predicate checkCallContextCall(CallContext cc, DataFlowCall call, DataFlowCallable calltarget) {
exists(DataFlowCall ctx | cc = TSpecificCall(ctx) |
if reducedViableImplInCallContext(call, _, ctx)
then calltarget = prunedViableImplInCallContext(call, ctx)
else any()
/** Holds if `call` does not have a reduced set of dispatch targets in call context `ctx`. */
bindingset[call, ctx]
predicate noPrunedViableImplInCallContext(DataFlowCall call, CallContext ctx) {
exists(DataFlowCall outer | ctx = TSpecificCall(outer) |
not reducedViableImplInCallContext(call, _, outer)
)
or
cc instanceof CallContextSomeCall
ctx instanceof CallContextSomeCall
or
cc instanceof CallContextAny
ctx instanceof CallContextAny
or
cc instanceof CallContextReturn
ctx instanceof CallContextReturn
}
/**
@@ -1320,11 +1306,7 @@ module MakeImplCommon<InputSig Lang> {
predicate resolveReturn(CallContext cc, DataFlowCallable callable, DataFlowCall call) {
cc instanceof CallContextAny and callable = viableCallableExt(call)
or
exists(DataFlowCallable c0, DataFlowCall call0 |
callEnclosingCallable(call0, callable) and
cc = TReturn(c0, call0) and
c0 = prunedViableImplInCallContextReverse(call0, call)
)
callable = prunedViableImplInCallContextReverse(call, cc)
}
/**
@@ -1333,17 +1315,10 @@ module MakeImplCommon<InputSig Lang> {
*/
bindingset[call, cc]
DataFlowCallable resolveCall(DataFlowCall call, CallContext cc) {
exists(DataFlowCall ctx | cc = TSpecificCall(ctx) |
if reducedViableImplInCallContext(call, _, ctx)
then result = prunedViableImplInCallContext(call, ctx)
else result = viableCallableExt(call)
)
result = prunedViableImplInCallContext(call, cc)
or
result = viableCallableExt(call) and cc instanceof CallContextSomeCall
or
result = viableCallableExt(call) and cc instanceof CallContextAny
or
result = viableCallableExt(call) and cc instanceof CallContextReturn
noPrunedViableImplInCallContext(call, cc) and
result = viableCallableExt(call)
}
/** An optional Boolean value. */