From c8046fa8e0fcb2caff7422bc5e0d2a82ec0d01c0 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 10 Dec 2024 11:25:27 +0100 Subject: [PATCH 01/14] Dataflow: Drop some ApApprox columns and joins. --- .../codeql/dataflow/internal/DataFlowImpl.qll | 113 ++++++++---------- 1 file changed, 48 insertions(+), 65 deletions(-) diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll index 313934378c63..635e8e24aee8 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll @@ -942,11 +942,9 @@ module MakeImpl Lang> { } pragma[nomagic] - predicate returnMayFlowThrough(RetNodeEx ret, Ap argAp, Ap ap, ReturnKindExt kind) { + predicate returnMayFlowThrough(RetNodeEx ret, ReturnKindExt kind) { throughFlowNodeCand(ret) and - kind = ret.getKind() and - exists(argAp) and - exists(ap) + kind = ret.getKind() } pragma[nomagic] @@ -969,11 +967,10 @@ module MakeImpl Lang> { predicate callEdgeReturn( DataFlowCall call, DataFlowCallable c, RetNodeEx ret, ReturnKindExt kind, NodeEx out, - boolean allowsFieldFlow, Ap ap + boolean allowsFieldFlow ) { flowOutOfCallNodeCand1(call, ret, kind, out, allowsFieldFlow) and - c = ret.getEnclosingCallable() and - exists(ap) + c = ret.getEnclosingCallable() } predicate relevantCallEdgeIn(DataFlowCall call, DataFlowCallable c) { @@ -981,7 +978,7 @@ module MakeImpl Lang> { } predicate relevantCallEdgeOut(DataFlowCall call, DataFlowCallable c) { - callEdgeReturn(call, c, _, _, _, _, _) + callEdgeReturn(call, c, _, _, _, _) } additional predicate stats( @@ -1004,7 +1001,7 @@ module MakeImpl Lang> { calledges = count(DataFlowCall call, DataFlowCallable c | callEdgeArgParam(call, c, _, _, _, _) or - callEdgeReturn(call, c, _, _, _, _, _) + callEdgeReturn(call, c, _, _, _, _) ) } /* End: Stage 1 logic. */ @@ -1287,7 +1284,7 @@ module MakeImpl Lang> { predicate parameterMayFlowThrough(ParamNodeEx p, Ap ap); - predicate returnMayFlowThrough(RetNodeEx ret, Ap argAp, Ap ap, ReturnKindExt kind); + predicate returnMayFlowThrough(RetNodeEx ret, ReturnKindExt kind); predicate storeStepCand( NodeEx node1, Ap ap1, Content c, NodeEx node2, DataFlowType contentType, @@ -1303,7 +1300,7 @@ module MakeImpl Lang> { predicate callEdgeReturn( DataFlowCall call, DataFlowCallable c, RetNodeEx ret, ReturnKindExt kind, NodeEx out, - boolean allowsFieldFlow, Ap ap + boolean allowsFieldFlow ); predicate relevantCallEdgeIn(DataFlowCall call, DataFlowCallable c); @@ -1437,13 +1434,12 @@ module MakeImpl Lang> { pragma[nomagic] private predicate flowThroughOutOfCall( - DataFlowCall call, CcCall ccc, RetNodeEx ret, NodeEx out, boolean allowsFieldFlow, - ApApprox argApa, ApApprox apa + DataFlowCall call, CcCall ccc, RetNodeEx ret, NodeEx out, boolean allowsFieldFlow ) { exists(ReturnKindExt kind | - PrevStage::callEdgeReturn(call, _, ret, kind, out, allowsFieldFlow, apa) and + PrevStage::callEdgeReturn(call, _, ret, kind, out, allowsFieldFlow) and PrevStage::callMayFlowThroughRev(call) and - PrevStage::returnMayFlowThrough(ret, argApa, apa, kind) and + PrevStage::returnMayFlowThrough(ret, kind) and matchesCall(ccc, call) ) } @@ -1560,12 +1556,9 @@ module MakeImpl Lang> { fwdFlowOut(_, _, node, state, cc, summaryCtx, t, ap, apa, stored) or // flow through a callable - exists( - DataFlowCall call, CcCall ccc, RetNodeEx ret, boolean allowsFieldFlow, - ApApprox innerArgApa - | - fwdFlowThrough(call, cc, state, ccc, summaryCtx, t, ap, apa, stored, ret, innerArgApa) and - flowThroughOutOfCall(call, ccc, ret, node, allowsFieldFlow, innerArgApa, apa) and + exists(DataFlowCall call, CcCall ccc, RetNodeEx ret, boolean allowsFieldFlow | + fwdFlowThrough(call, cc, state, ccc, summaryCtx, t, ap, apa, stored, ret, _) and + flowThroughOutOfCall(call, ccc, ret, node, allowsFieldFlow) and not inBarrier(node, state) and if allowsFieldFlow = false then ap instanceof ApNil else any() ) @@ -1925,7 +1918,7 @@ module MakeImpl Lang> { DataFlowCallable c, CcNoCall ctx ) { result = viableImplCallContextReducedReverse(c, ctx) and - PrevStage::callEdgeReturn(result, c, _, _, _, _, _) + PrevStage::callEdgeReturn(result, c, _, _, _, _) } bindingset[c, ctx] @@ -1939,21 +1932,20 @@ module MakeImpl Lang> { bindingset[call] pragma[inline_late] private predicate flowOutOfCallApaInlineLate( - DataFlowCall call, DataFlowCallable c, RetNodeEx ret, NodeEx out, boolean allowsFieldFlow, - ApApprox apa + DataFlowCall call, DataFlowCallable c, RetNodeEx ret, NodeEx out, boolean allowsFieldFlow ) { - PrevStage::callEdgeReturn(call, c, ret, _, out, allowsFieldFlow, apa) + PrevStage::callEdgeReturn(call, c, ret, _, out, allowsFieldFlow) } - bindingset[c, ret, apa, innercc] + bindingset[c, ret, innercc] pragma[inline_late] pragma[noopt] private predicate flowOutOfCallApaNotCallContextReduced( DataFlowCall call, DataFlowCallable c, RetNodeEx ret, NodeEx out, boolean allowsFieldFlow, - ApApprox apa, CcNoCall innercc + CcNoCall innercc ) { viableImplNotCallContextReducedReverse(innercc) and - PrevStage::callEdgeReturn(call, c, ret, _, out, allowsFieldFlow, apa) + PrevStage::callEdgeReturn(call, c, ret, _, out, allowsFieldFlow) } pragma[nomagic] @@ -1975,10 +1967,9 @@ module MakeImpl Lang> { inner = ret.getEnclosingCallable() and ( call = viableImplCallContextReducedReverseInlineLate(inner, innercc) and - flowOutOfCallApaInlineLate(call, inner, ret, out, allowsFieldFlow, apa) + flowOutOfCallApaInlineLate(call, inner, ret, out, allowsFieldFlow) or - flowOutOfCallApaNotCallContextReduced(call, inner, ret, out, allowsFieldFlow, apa, - innercc) + flowOutOfCallApaNotCallContextReduced(call, inner, ret, out, allowsFieldFlow, innercc) ) } @@ -2050,10 +2041,8 @@ module MakeImpl Lang> { private predicate fwdFlow1Out( NodeEx node, FlowState state, Cc cc, Typ t0, Ap ap, TypOption stored ) { - exists(ApApprox apa | - fwdFlow1(node, state, cc, _, t0, _, ap, apa, stored) and - PrevStage::callEdgeReturn(_, _, _, _, node, _, apa) - ) + fwdFlow1(node, state, cc, _, t0, _, ap, _, stored) and + PrevStage::callEdgeReturn(_, _, _, _, node, _) } pragma[nomagic] @@ -2097,15 +2086,14 @@ module MakeImpl Lang> { ) { exists(ReturnKindExt kind, ParamNodeEx p, Ap argAp | instanceofCcCall(ccc) and - fwdFlow(pragma[only_bind_into](ret), state, ccc, summaryCtx, t, ap, - pragma[only_bind_into](apa), stored) and + fwdFlow(pragma[only_bind_into](ret), state, ccc, summaryCtx, t, ap, apa, stored) and summaryCtx = TSummaryCtxSome(pragma[only_bind_into](p), _, _, pragma[only_bind_into](argAp), _) and not outBarrier(ret, state) and kind = ret.getKind() and parameterFlowThroughAllowed(p, kind) and argApa = getApprox(argAp) and - PrevStage::returnMayFlowThrough(ret, pragma[only_bind_into](argApa), apa, kind) + PrevStage::returnMayFlowThrough(ret, kind) ) } @@ -2178,10 +2166,10 @@ module MakeImpl Lang> { RetNodeEx ret, ReturnPosition pos, FlowState state, CcCall ccc, ParamNodeEx p, Typ argT, Ap argAp, ApApprox argApa, TypOption argStored, Ap ap ) { - exists(DataFlowCall call, ApApprox apa, boolean allowsFieldFlow | - returnFlowsThrough0(call, state, ccc, ap, apa, ret, + exists(DataFlowCall call, boolean allowsFieldFlow | + returnFlowsThrough0(call, state, ccc, ap, _, ret, TSummaryCtxSome(p, _, argT, argAp, argStored), argApa) and - flowThroughOutOfCall(call, ccc, ret, _, allowsFieldFlow, argApa, apa) and + flowThroughOutOfCall(call, ccc, ret, _, allowsFieldFlow) and pos = ret.getReturnPosition() and if allowsFieldFlow = false then ap instanceof ApNil else any() ) @@ -2216,14 +2204,13 @@ module MakeImpl Lang> { pragma[nomagic] private predicate flowOutOfCallAp( DataFlowCall call, DataFlowCallable c, RetNodeEx ret, ReturnPosition pos, NodeEx out, - Ap ap + Ap ap, boolean allowsFieldFlow ) { - exists(ApApprox apa, boolean allowsFieldFlow | - PrevStage::callEdgeReturn(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() - | + PrevStage::callEdgeReturn(call, c, ret, _, out, allowsFieldFlow) and + fwdFlow(ret, _, _, _, _, ap, _, _) and + pos = ret.getReturnPosition() and + (if allowsFieldFlow = false then ap instanceof ApNil else any()) and + ( // both directions are needed for flow-through FwdTypeFlowInput::dataFlowTakenCallEdgeIn(call, c, _) or FwdTypeFlowInput::dataFlowTakenCallEdgeOut(call, c) @@ -2356,7 +2343,7 @@ module MakeImpl Lang> { predicate enableTypeFlow = Param::enableTypeFlow/0; predicate relevantCallEdgeIn(DataFlowCall call, DataFlowCallable c) { - flowOutOfCallAp(call, c, _, _, _, _) + flowOutOfCallAp(call, c, _, _, _, _, _) } predicate relevantCallEdgeOut(DataFlowCall call, DataFlowCallable c) { @@ -2407,7 +2394,7 @@ module MakeImpl Lang> { DataFlowCall call, RetNodeEx ret, ReturnPosition pos, NodeEx out, Ap ap, boolean cc ) { exists(DataFlowCallable c | - flowOutOfCallAp(call, c, ret, pos, out, ap) and + flowOutOfCallAp(call, c, ret, pos, out, ap, _) and RevTypeFlow::typeFlowValidEdgeIn(call, c, cc) ) } @@ -2559,8 +2546,8 @@ module MakeImpl Lang> { } pragma[nomagic] - predicate returnMayFlowThrough(RetNodeEx ret, Ap argAp, Ap ap, ReturnKindExt kind) { - exists(ParamNodeEx p, ReturnPosition pos | + predicate returnMayFlowThrough(RetNodeEx ret, ReturnKindExt kind) { + exists(ParamNodeEx p, ReturnPosition pos, Ap argAp, Ap ap | returnFlowsThrough(ret, pos, _, _, p, _, argAp, _, _, ap) and parameterFlowsThroughRev(p, argAp, pos, ap) and kind = pos.getKind() @@ -2607,14 +2594,13 @@ module MakeImpl Lang> { predicate callEdgeReturn( DataFlowCall call, DataFlowCallable c, RetNodeEx ret, ReturnKindExt kind, NodeEx out, - boolean allowsFieldFlow, Ap ap + boolean allowsFieldFlow ) { - exists(FlowState state, ReturnPosition pos | - flowOutOfCallAp(call, c, ret, pos, out, ap) and + exists(FlowState state, ReturnPosition pos, Ap ap | + flowOutOfCallAp(call, c, ret, pos, out, ap, allowsFieldFlow) and revFlow(ret, pragma[only_bind_into](state), pragma[only_bind_into](ap)) and revFlow(out, pragma[only_bind_into](state), pragma[only_bind_into](ap)) and kind = pos.getKind() and - allowsFieldFlow = true and RevTypeFlowInput::dataFlowTakenCallEdgeIn(call, c, _) ) } @@ -2624,7 +2610,7 @@ module MakeImpl Lang> { } predicate relevantCallEdgeOut(DataFlowCall call, DataFlowCallable c) { - callEdgeReturn(call, c, _, _, _, _, _) + callEdgeReturn(call, c, _, _, _, _) } /** Holds if `node1` can step to `node2` in one or more local steps. */ @@ -2719,7 +2705,7 @@ module MakeImpl Lang> { callEdgeArgParam(_, _, node, next, _, ap) and apNext = ap or - callEdgeReturn(_, _, node, _, next, _, ap) and + callEdgeReturn(_, _, node, _, next, _) and apNext = ap or storeStepCand(node, _, _, next, _, _) @@ -3206,13 +3192,10 @@ module MakeImpl Lang> { PathNodeImpl pn1, PathNodeImpl pn2, PathNodeImpl pn3, NodeEx node, Cc cc, FlowState state, SummaryCtx summaryCtx, Typ t, Ap ap, TypOption stored ) { - exists( - DataFlowCall call, CcCall ccc, RetNodeEx ret, boolean allowsFieldFlow, - ApApprox innerArgApa, ApApprox apa - | - fwdFlowThroughStep1(pn1, pn2, pn3, call, cc, state, ccc, summaryCtx, t, ap, apa, - stored, ret, innerArgApa) and - flowThroughOutOfCall(call, ccc, ret, node, allowsFieldFlow, innerArgApa, apa) and + exists(DataFlowCall call, CcCall ccc, RetNodeEx ret, boolean allowsFieldFlow | + fwdFlowThroughStep1(pn1, pn2, pn3, call, cc, state, ccc, summaryCtx, t, ap, _, stored, + ret, _) and + flowThroughOutOfCall(call, ccc, ret, node, allowsFieldFlow) and not inBarrier(node, state) and if allowsFieldFlow = false then ap instanceof ApNil else any() ) From 7c888ebe062c41026e112e92cf5ca0bfaff1314c Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 10 Dec 2024 11:43:01 +0100 Subject: [PATCH 02/14] Dataflow: Replace some allowsFieldFlow,apa pairs with emptyAp boolean. --- .../codeql/dataflow/internal/DataFlowImpl.qll | 142 +++++++++--------- 1 file changed, 68 insertions(+), 74 deletions(-) diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll index 635e8e24aee8..b3563d958618 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll @@ -931,12 +931,12 @@ module MakeImpl Lang> { * candidate for the origin of a summary. */ pragma[nomagic] - predicate parameterMayFlowThrough(ParamNodeEx p, Ap ap) { + predicate parameterMayFlowThrough(ParamNodeEx p, boolean emptyAp) { exists(DataFlowCallable c, ReturnKindExt kind | throughFlowNodeCand(p) and returnFlowCallableNodeCand(c, kind) and p.getEnclosingCallable() = c and - exists(ap) and + emptyAp = [true, false] and parameterFlowThroughAllowed(p, kind) ) } @@ -957,12 +957,17 @@ module MakeImpl Lang> { } predicate callEdgeArgParam( - DataFlowCall call, DataFlowCallable c, ArgNodeEx arg, ParamNodeEx p, - boolean allowsFieldFlow, Ap ap + DataFlowCall call, DataFlowCallable c, ArgNodeEx arg, ParamNodeEx p, boolean emptyAp ) { - flowIntoCallNodeCand1(call, arg, p, allowsFieldFlow) and - c = p.getEnclosingCallable() and - exists(ap) + exists(boolean allowsFieldFlow | + flowIntoCallNodeCand1(call, arg, p, allowsFieldFlow) and + c = p.getEnclosingCallable() and + ( + emptyAp = true + or + allowsFieldFlow = true and emptyAp = false + ) + ) } predicate callEdgeReturn( @@ -974,7 +979,7 @@ module MakeImpl Lang> { } predicate relevantCallEdgeIn(DataFlowCall call, DataFlowCallable c) { - callEdgeArgParam(call, c, _, _, _, _) + callEdgeArgParam(call, c, _, _, _) } predicate relevantCallEdgeOut(DataFlowCall call, DataFlowCallable c) { @@ -1000,7 +1005,7 @@ module MakeImpl Lang> { tuples = count(NodeEx n, boolean b | revFlow(n, b)) and calledges = count(DataFlowCall call, DataFlowCallable c | - callEdgeArgParam(call, c, _, _, _, _) or + callEdgeArgParam(call, c, _, _, _) or callEdgeReturn(call, c, _, _, _, _) ) } @@ -1282,7 +1287,7 @@ module MakeImpl Lang> { predicate callMayFlowThroughRev(DataFlowCall call); - predicate parameterMayFlowThrough(ParamNodeEx p, Ap ap); + predicate parameterMayFlowThrough(ParamNodeEx p, boolean emptyAp); predicate returnMayFlowThrough(RetNodeEx ret, ReturnKindExt kind); @@ -1294,8 +1299,7 @@ module MakeImpl Lang> { predicate readStepCand(NodeEx n1, Content c, NodeEx n2); predicate callEdgeArgParam( - DataFlowCall call, DataFlowCallable c, ArgNodeEx arg, ParamNodeEx p, - boolean allowsFieldFlow, Ap ap + DataFlowCall call, DataFlowCallable c, ArgNodeEx arg, ParamNodeEx p, boolean emptyAp ); predicate callEdgeReturn( @@ -1732,34 +1736,19 @@ module MakeImpl Lang> { private module FwdFlowIn { pragma[nomagic] private predicate callEdgeArgParamRestricted( - DataFlowCall call, DataFlowCallable c, ArgNodeEx arg, ParamNodeEx p, boolean emptyAp, - ApApprox apa + DataFlowCall call, DataFlowCallable c, ArgNodeEx arg, ParamNodeEx p, boolean emptyAp ) { - exists(boolean allowsFieldFlow | - PrevStage::callEdgeArgParam(call, c, arg, p, allowsFieldFlow, apa) - | - if - PrevStage::callMayFlowThroughRev(call) and - PrevStage::parameterMayFlowThrough(p, apa) - then - emptyAp = true and - apa instanceof PrevStage::ApNil and - flowThrough() - or - emptyAp = false and - allowsFieldFlow = true and - if allowsFieldFlowThrough(call, c) then flowThrough() else not flowThrough() - else ( - not flowThrough() and - ( - emptyAp = true and - apa instanceof PrevStage::ApNil - or - emptyAp = false and - allowsFieldFlow = true - ) - ) - ) + PrevStage::callEdgeArgParam(call, c, arg, p, emptyAp) and + if + PrevStage::callMayFlowThroughRev(call) and + PrevStage::parameterMayFlowThrough(p, emptyAp) + then + emptyAp = true and + flowThrough() + or + emptyAp = false and + if allowsFieldFlowThrough(call, c) then flowThrough() else not flowThrough() + else not flowThrough() } pragma[nomagic] @@ -1767,7 +1756,7 @@ module MakeImpl Lang> { DataFlowCall call, CcCall ctx ) { result = viableImplCallContextReduced(call, ctx) and - callEdgeArgParamRestricted(call, result, _, _, _, _) + callEdgeArgParamRestricted(call, result, _, _, _) } bindingset[call, ctx] @@ -1783,7 +1772,7 @@ module MakeImpl Lang> { private DataFlowCallable viableImplCallContextReducedInlineLate( DataFlowCall call, ArgNodeEx arg, CcCall ctx ) { - callEdgeArgParamRestricted(call, _, arg, _, _, _) and + callEdgeArgParamRestricted(call, _, arg, _, _) and instanceofCcCall(ctx) and result = viableImplCallContextReducedInlineLate(call, ctx) } @@ -1791,10 +1780,9 @@ module MakeImpl Lang> { bindingset[call] pragma[inline_late] private predicate callEdgeArgParamRestrictedInlineLate( - DataFlowCall call, DataFlowCallable c, ArgNodeEx arg, ParamNodeEx p, boolean emptyAp, - ApApprox apa + DataFlowCall call, DataFlowCallable c, ArgNodeEx arg, ParamNodeEx p, boolean emptyAp ) { - callEdgeArgParamRestricted(call, c, arg, p, emptyAp, apa) + callEdgeArgParamRestricted(call, c, arg, p, emptyAp) } bindingset[call, ctx] @@ -1809,7 +1797,7 @@ module MakeImpl Lang> { private predicate viableImplArgNotCallContextReduced( DataFlowCall call, ArgNodeEx arg, Cc outercc ) { - callEdgeArgParamRestricted(call, _, arg, _, _, _) and + callEdgeArgParamRestricted(call, _, arg, _, _) and instanceofCc(outercc) and viableImplNotCallContextReducedInlineLate(call, outercc) } @@ -1828,7 +1816,7 @@ module MakeImpl Lang> { ) and not outBarrier(arg, state) and not inBarrier(p, state) and - callEdgeArgParamRestrictedInlineLate(call, inner, arg, p, emptyAp, apa) + callEdgeArgParamRestrictedInlineLate(call, inner, arg, p, emptyAp) } pragma[inline] @@ -2072,10 +2060,9 @@ module MakeImpl Lang> { private module FwdTypeFlow = TypeFlow; private predicate flowIntoCallApaTaken( - DataFlowCall call, DataFlowCallable c, ArgNodeEx arg, ParamNodeEx p, - boolean allowsFieldFlow, ApApprox apa + DataFlowCall call, DataFlowCallable c, ArgNodeEx arg, ParamNodeEx p, boolean emptyAp ) { - PrevStage::callEdgeArgParam(call, c, arg, p, allowsFieldFlow, apa) and + PrevStage::callEdgeArgParam(call, c, arg, p, emptyAp) and FwdTypeFlowInput::dataFlowTakenCallEdgeIn(call, c, _) } @@ -2177,16 +2164,16 @@ module MakeImpl Lang> { pragma[nomagic] private predicate flowThroughIntoCall( - DataFlowCall call, ArgNodeEx arg, ParamNodeEx p, boolean allowsFieldFlow, Ap argAp, Ap ap + DataFlowCall call, ArgNodeEx arg, ParamNodeEx p, Ap argAp, Ap ap ) { - exists(ApApprox argApa, Typ argT, TypOption argStored | + exists(ApApprox argApa, Typ argT, TypOption argStored, boolean emptyArgAp | returnFlowsThrough(_, _, _, _, pragma[only_bind_into](p), pragma[only_bind_into](argT), pragma[only_bind_into](argAp), pragma[only_bind_into](argApa), pragma[only_bind_into](argStored), ap) and - flowIntoCallApaTaken(call, _, pragma[only_bind_into](arg), p, allowsFieldFlow, argApa) and + flowIntoCallApaTaken(call, _, pragma[only_bind_into](arg), p, emptyArgAp) and fwdFlow(arg, _, _, _, pragma[only_bind_into](argT), pragma[only_bind_into](argAp), pragma[only_bind_into](argApa), pragma[only_bind_into](argStored)) and - if allowsFieldFlow = false then argAp instanceof ApNil else any() + if argAp instanceof ApNil then emptyArgAp = true else emptyArgAp = false ) } @@ -2194,10 +2181,10 @@ module MakeImpl Lang> { private predicate flowIntoCallAp( DataFlowCall call, DataFlowCallable c, ArgNodeEx arg, ParamNodeEx p, Ap ap ) { - exists(ApApprox apa, boolean allowsFieldFlow | - flowIntoCallApaTaken(call, c, arg, p, allowsFieldFlow, apa) and - fwdFlow(arg, _, _, _, _, ap, apa, _) and - if allowsFieldFlow = false then ap instanceof ApNil else any() + exists(boolean emptyAp | + flowIntoCallApaTaken(call, c, arg, p, emptyAp) and + fwdFlow(arg, _, _, _, _, ap, _, _) and + if ap instanceof ApNil then emptyAp = true else emptyAp = false ) } @@ -2282,7 +2269,7 @@ module MakeImpl Lang> { // flow through a callable exists(DataFlowCall call, ParamNodeEx p, Ap innerReturnAp | revFlowThrough(call, returnCtx, p, state, _, returnAp, ap, innerReturnAp) and - flowThroughIntoCall(call, node, p, _, ap, innerReturnAp) + flowThroughIntoCall(call, node, p, ap, innerReturnAp) ) or // flow out of a callable @@ -2424,10 +2411,13 @@ module MakeImpl Lang> { private predicate revFlowParamToReturn( ParamNodeEx p, FlowState state, ReturnPosition pos, Ap returnAp, Ap ap ) { - revFlow(pragma[only_bind_into](p), state, TReturnCtxMaybeFlowThrough(pos), - apSome(returnAp), pragma[only_bind_into](ap)) and - parameterFlowThroughAllowed(p, pos.getKind()) and - PrevStage::parameterMayFlowThrough(p, getApprox(ap)) + exists(boolean emptyAp | + revFlow(pragma[only_bind_into](p), state, TReturnCtxMaybeFlowThrough(pos), + apSome(returnAp), pragma[only_bind_into](ap)) and + parameterFlowThroughAllowed(p, pos.getKind()) and + PrevStage::parameterMayFlowThrough(p, emptyAp) and + if ap instanceof ApNil then emptyAp = true else emptyAp = false + ) } pragma[nomagic] @@ -2517,13 +2507,21 @@ module MakeImpl Lang> { } pragma[nomagic] - predicate parameterMayFlowThrough(ParamNodeEx p, Ap ap) { + private predicate parameterMayFlowThroughAp(ParamNodeEx p, Ap ap) { exists(ReturnPosition pos | returnFlowsThrough(_, pos, _, _, p, _, ap, _, _, _) and parameterFlowsThroughRev(p, ap, pos, _) ) } + pragma[nomagic] + predicate parameterMayFlowThrough(ParamNodeEx p, boolean emptyAp) { + exists(Ap ap | + parameterMayFlowThroughAp(p, ap) and + if ap instanceof ApNil then emptyAp = true else emptyAp = false + ) + } + pragma[nomagic] private predicate nodeMayUseSummary0(NodeEx n, ParamNodeEx p, FlowState state, Ap ap) { exists(Ap ap0 | @@ -2540,7 +2538,7 @@ module MakeImpl Lang> { pragma[nomagic] additional predicate nodeMayUseSummary(NodeEx n, FlowState state, Ap ap) { exists(ParamNodeEx p | - parameterMayFlowThrough(p, ap) and + parameterMayFlowThroughAp(p, ap) and nodeMayUseSummary0(n, p, state, ap) ) } @@ -2561,7 +2559,7 @@ module MakeImpl Lang> { ) { exists(ParamNodeEx p, Ap innerReturnAp | revFlowThrough(call, returnCtx, p, state, _, returnAp, ap, innerReturnAp) and - flowThroughIntoCall(call, arg, p, _, ap, innerReturnAp) + flowThroughIntoCall(call, arg, p, ap, innerReturnAp) ) } @@ -2574,17 +2572,13 @@ module MakeImpl Lang> { } predicate callEdgeArgParam( - DataFlowCall call, DataFlowCallable c, ArgNodeEx arg, ParamNodeEx p, - boolean allowsFieldFlow, Ap ap + DataFlowCall call, DataFlowCallable c, ArgNodeEx arg, ParamNodeEx p, boolean emptyAp ) { - exists(FlowState state | + exists(FlowState state, Ap ap | flowIntoCallAp(call, c, arg, p, ap) and revFlow(arg, pragma[only_bind_into](state), pragma[only_bind_into](ap)) and revFlow(p, pragma[only_bind_into](state), pragma[only_bind_into](ap)) and - // allowsFieldFlow has already been checked in flowIntoCallAp, since - // `Ap` is at least as precise as a boolean from Stage 2 and - // forward, so no need to check it again later. - allowsFieldFlow = true + if ap instanceof ApNil then emptyAp = true else emptyAp = false | // both directions are needed for flow-through RevTypeFlowInput::dataFlowTakenCallEdgeIn(call, c, _) or @@ -2606,7 +2600,7 @@ module MakeImpl Lang> { } predicate relevantCallEdgeIn(DataFlowCall call, DataFlowCallable c) { - callEdgeArgParam(call, c, _, _, _, _) + callEdgeArgParam(call, c, _, _, _) } predicate relevantCallEdgeOut(DataFlowCall call, DataFlowCallable c) { @@ -2702,7 +2696,7 @@ module MakeImpl Lang> { apNext = ap and ap instanceof ApNil or - callEdgeArgParam(_, _, node, next, _, ap) and + callEdgeArgParam(_, _, node, next, _) and apNext = ap or callEdgeReturn(_, _, node, _, next, _) and From d4044062c511096b0f33899e876bb6e459cda7e0 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 10 Dec 2024 12:38:10 +0100 Subject: [PATCH 03/14] Dataflow: Remove ApApprox column in out-flow. --- .../codeql/dataflow/internal/DataFlowImpl.qll | 29 ++++++++++--------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll index b3563d958618..4db25288eeb4 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll @@ -1557,7 +1557,8 @@ module MakeImpl Lang> { summaryCtx = TSummaryCtxSome(node, state, t, ap, stored) or // flow out of a callable - fwdFlowOut(_, _, node, state, cc, summaryCtx, t, ap, apa, stored) + fwdFlowOut(_, _, node, state, cc, summaryCtx, t, ap, stored) and + apa = getApprox(ap) or // flow through a callable exists(DataFlowCall call, CcCall ccc, RetNodeEx ret, boolean allowsFieldFlow | @@ -1939,19 +1940,19 @@ module MakeImpl Lang> { pragma[nomagic] private predicate fwdFlowIntoRet( RetNodeEx ret, FlowState state, CcNoCall cc, SummaryCtx summaryCtx, Typ t, Ap ap, - ApApprox apa, TypOption stored + TypOption stored ) { instanceofCcNoCall(cc) and not outBarrier(ret, state) and - fwdFlow(ret, state, cc, summaryCtx, t, ap, apa, stored) + fwdFlow(ret, state, cc, summaryCtx, t, ap, _, stored) } pragma[nomagic] private predicate fwdFlowOutCand( DataFlowCall call, RetNodeEx ret, CcNoCall innercc, DataFlowCallable inner, NodeEx out, - ApApprox apa, boolean allowsFieldFlow + boolean allowsFieldFlow ) { - fwdFlowIntoRet(ret, _, innercc, _, _, _, apa, _) and + fwdFlowIntoRet(ret, _, innercc, _, _, _, _) and inner = ret.getEnclosingCallable() and ( call = viableImplCallContextReducedReverseInlineLate(inner, innercc) and @@ -1964,9 +1965,9 @@ module MakeImpl Lang> { pragma[nomagic] private predicate fwdFlowOutValidEdge( DataFlowCall call, RetNodeEx ret, CcNoCall innercc, DataFlowCallable inner, NodeEx out, - CcNoCall outercc, ApApprox apa, boolean allowsFieldFlow + CcNoCall outercc, boolean allowsFieldFlow ) { - fwdFlowOutCand(call, ret, innercc, inner, out, apa, allowsFieldFlow) and + fwdFlowOutCand(call, ret, innercc, inner, out, allowsFieldFlow) and FwdTypeFlow::typeFlowValidEdgeOut(call, inner) and outercc = getCallContextReturn(inner, call) } @@ -1974,11 +1975,11 @@ module MakeImpl Lang> { pragma[inline] private predicate fwdFlowOut( DataFlowCall call, DataFlowCallable inner, NodeEx out, FlowState state, CcNoCall outercc, - SummaryCtx summaryCtx, Typ t, Ap ap, ApApprox apa, TypOption stored + SummaryCtx summaryCtx, Typ t, Ap ap, TypOption stored ) { exists(RetNodeEx ret, CcNoCall innercc, boolean allowsFieldFlow | - fwdFlowIntoRet(ret, state, innercc, summaryCtx, t, ap, apa, stored) and - fwdFlowOutValidEdge(call, ret, innercc, inner, out, outercc, apa, allowsFieldFlow) and + fwdFlowIntoRet(ret, state, innercc, summaryCtx, t, ap, stored) and + fwdFlowOutValidEdge(call, ret, innercc, inner, out, outercc, allowsFieldFlow) and not inBarrier(out, state) and if allowsFieldFlow = false then ap instanceof ApNil else any() ) @@ -2022,7 +2023,7 @@ module MakeImpl Lang> { DataFlowCall call, DataFlowCallable c, NodeEx node, FlowState state, Cc cc, Typ t, Ap ap, TypOption stored ) { - fwdFlowOut(call, c, node, state, cc, _, t, ap, _, stored) + fwdFlowOut(call, c, node, state, cc, _, t, ap, stored) } pragma[nomagic] @@ -3299,10 +3300,10 @@ module MakeImpl Lang> { ) or // flow out of a callable - exists(RetNodeEx ret, CcNoCall innercc, boolean allowsFieldFlow, ApApprox apa | + exists(RetNodeEx ret, CcNoCall innercc, boolean allowsFieldFlow | pn1 = TPathNodeMid(ret, state, innercc, summaryCtx, t, ap, stored) and - fwdFlowIntoRet(ret, state, innercc, summaryCtx, t, ap, apa, stored) and - fwdFlowOutValidEdge(_, ret, innercc, _, node, cc, apa, allowsFieldFlow) and + fwdFlowIntoRet(ret, state, innercc, summaryCtx, t, ap, stored) and + fwdFlowOutValidEdge(_, ret, innercc, _, node, cc, allowsFieldFlow) and not inBarrier(node, state) and label = "" and if allowsFieldFlow = false then ap instanceof ApNil else any() From 262f64f03751b93fc4a4df52e252561a0bc3471f Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 10 Dec 2024 12:42:07 +0100 Subject: [PATCH 04/14] Dataflow: Remove unused columns. --- .../codeql/dataflow/internal/DataFlowImpl.qll | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll index 4db25288eeb4..564810f0951f 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll @@ -1562,7 +1562,7 @@ module MakeImpl Lang> { or // flow through a callable exists(DataFlowCall call, CcCall ccc, RetNodeEx ret, boolean allowsFieldFlow | - fwdFlowThrough(call, cc, state, ccc, summaryCtx, t, ap, apa, stored, ret, _) and + fwdFlowThrough(call, cc, state, ccc, summaryCtx, t, ap, apa, stored, ret) and flowThroughOutOfCall(call, ccc, ret, node, allowsFieldFlow) and not inBarrier(node, state) and if allowsFieldFlow = false then ap instanceof ApNil else any() @@ -2098,10 +2098,9 @@ module MakeImpl Lang> { pragma[nomagic] private predicate fwdFlowThrough( DataFlowCall call, Cc cc, FlowState state, CcCall ccc, SummaryCtx summaryCtx, Typ t, - Ap ap, ApApprox apa, TypOption stored, RetNodeEx ret, ApApprox innerArgApa + Ap ap, ApApprox apa, TypOption stored, RetNodeEx ret ) { - fwdFlowThrough0(call, _, cc, state, ccc, summaryCtx, t, ap, apa, stored, ret, _, - innerArgApa) + fwdFlowThrough0(call, _, cc, state, ccc, summaryCtx, t, ap, apa, stored, ret, _, _) } pragma[nomagic] @@ -3136,10 +3135,10 @@ module MakeImpl Lang> { private predicate fwdFlowThroughStep0( DataFlowCall call, ArgNodeEx arg, Cc cc, FlowState state, CcCall ccc, SummaryCtx summaryCtx, Typ t, Ap ap, ApApprox apa, TypOption stored, RetNodeEx ret, - SummaryCtxSome innerSummaryCtx, ApApprox innerArgApa + SummaryCtxSome innerSummaryCtx ) { fwdFlowThrough0(call, arg, cc, state, ccc, summaryCtx, t, ap, apa, stored, ret, - innerSummaryCtx, innerArgApa) + innerSummaryCtx, _) } bindingset[node, state, cc, summaryCtx, t, ap, stored] @@ -3165,14 +3164,14 @@ module MakeImpl Lang> { private predicate fwdFlowThroughStep1( PathNodeImpl pn1, PathNodeImpl pn2, PathNodeImpl pn3, DataFlowCall call, Cc cc, FlowState state, CcCall ccc, SummaryCtx summaryCtx, Typ t, Ap ap, ApApprox apa, - TypOption stored, RetNodeEx ret, ApApprox innerArgApa + TypOption stored, RetNodeEx ret ) { exists( FlowState state0, ArgNodeEx arg, SummaryCtxSome innerSummaryCtx, ParamNodeEx p, Typ innerArgT, Ap innerArgAp, TypOption innerArgStored | fwdFlowThroughStep0(call, arg, cc, state, ccc, summaryCtx, t, ap, apa, stored, ret, - innerSummaryCtx, innerArgApa) and + innerSummaryCtx) and innerSummaryCtx = TSummaryCtxSome(p, state0, innerArgT, innerArgAp, innerArgStored) and pn1 = mkPathNode(arg, state0, cc, summaryCtx, innerArgT, innerArgAp, innerArgStored) and pn2 = @@ -3189,7 +3188,7 @@ module MakeImpl Lang> { ) { exists(DataFlowCall call, CcCall ccc, RetNodeEx ret, boolean allowsFieldFlow | fwdFlowThroughStep1(pn1, pn2, pn3, call, cc, state, ccc, summaryCtx, t, ap, _, stored, - ret, _) and + ret) and flowThroughOutOfCall(call, ccc, ret, node, allowsFieldFlow) and not inBarrier(node, state) and if allowsFieldFlow = false then ap instanceof ApNil else any() From 882a9857881a11180b253a95e61a552745925f74 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 10 Dec 2024 12:43:24 +0100 Subject: [PATCH 05/14] Dataflow: Remove useless join. --- .../dataflow/codeql/dataflow/internal/DataFlowImpl.qll | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll index 564810f0951f..914a24dbe2f8 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll @@ -2166,13 +2166,12 @@ module MakeImpl Lang> { private predicate flowThroughIntoCall( DataFlowCall call, ArgNodeEx arg, ParamNodeEx p, Ap argAp, Ap ap ) { - exists(ApApprox argApa, Typ argT, TypOption argStored, boolean emptyArgAp | + exists(Typ argT, TypOption argStored, boolean emptyArgAp | returnFlowsThrough(_, _, _, _, pragma[only_bind_into](p), pragma[only_bind_into](argT), - pragma[only_bind_into](argAp), pragma[only_bind_into](argApa), - pragma[only_bind_into](argStored), ap) and + pragma[only_bind_into](argAp), _, pragma[only_bind_into](argStored), ap) and flowIntoCallApaTaken(call, _, pragma[only_bind_into](arg), p, emptyArgAp) and - fwdFlow(arg, _, _, _, pragma[only_bind_into](argT), pragma[only_bind_into](argAp), - pragma[only_bind_into](argApa), pragma[only_bind_into](argStored)) and + fwdFlow(arg, _, _, _, pragma[only_bind_into](argT), pragma[only_bind_into](argAp), _, + pragma[only_bind_into](argStored)) and if argAp instanceof ApNil then emptyArgAp = true else emptyArgAp = false ) } From a77adadd0179323fa33b376da00bdc349bb27a86 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 10 Dec 2024 12:46:30 +0100 Subject: [PATCH 06/14] Dataflow: Remove more unused columns. --- .../codeql/dataflow/internal/DataFlowImpl.qll | 48 +++++++++---------- 1 file changed, 23 insertions(+), 25 deletions(-) diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll index 914a24dbe2f8..6b24db3ea0c5 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll @@ -2069,8 +2069,8 @@ module MakeImpl Lang> { pragma[nomagic] private predicate fwdFlowRetFromArg( - RetNodeEx ret, FlowState state, CcCall ccc, SummaryCtxSome summaryCtx, ApApprox argApa, - Typ t, Ap ap, ApApprox apa, TypOption stored + RetNodeEx ret, FlowState state, CcCall ccc, SummaryCtxSome summaryCtx, Typ t, Ap ap, + ApApprox apa, TypOption stored ) { exists(ReturnKindExt kind, ParamNodeEx p, Ap argAp | instanceofCcCall(ccc) and @@ -2080,7 +2080,6 @@ module MakeImpl Lang> { not outBarrier(ret, state) and kind = ret.getKind() and parameterFlowThroughAllowed(p, kind) and - argApa = getApprox(argAp) and PrevStage::returnMayFlowThrough(ret, kind) ) } @@ -2089,9 +2088,9 @@ module MakeImpl Lang> { private predicate fwdFlowThrough0( DataFlowCall call, ArgNodeEx arg, Cc cc, FlowState state, CcCall ccc, SummaryCtx summaryCtx, Typ t, Ap ap, ApApprox apa, TypOption stored, RetNodeEx ret, - SummaryCtxSome innerSummaryCtx, ApApprox innerArgApa + SummaryCtxSome innerSummaryCtx ) { - fwdFlowRetFromArg(ret, state, ccc, innerSummaryCtx, innerArgApa, t, ap, apa, stored) and + fwdFlowRetFromArg(ret, state, ccc, innerSummaryCtx, t, ap, apa, stored) and fwdFlowIsEntered(call, arg, cc, ccc, summaryCtx, innerSummaryCtx) } @@ -2100,7 +2099,7 @@ module MakeImpl Lang> { DataFlowCall call, Cc cc, FlowState state, CcCall ccc, SummaryCtx summaryCtx, Typ t, Ap ap, ApApprox apa, TypOption stored, RetNodeEx ret ) { - fwdFlowThrough0(call, _, cc, state, ccc, summaryCtx, t, ap, apa, stored, ret, _, _) + fwdFlowThrough0(call, _, cc, state, ccc, summaryCtx, t, ap, apa, stored, ret, _) } pragma[nomagic] @@ -2141,21 +2140,20 @@ module MakeImpl Lang> { pragma[nomagic] private predicate returnFlowsThrough0( - DataFlowCall call, FlowState state, CcCall ccc, Ap ap, ApApprox apa, RetNodeEx ret, - SummaryCtxSome innerSummaryCtx, ApApprox innerArgApa + DataFlowCall call, FlowState state, CcCall ccc, Ap ap, RetNodeEx ret, + SummaryCtxSome innerSummaryCtx ) { - fwdFlowThrough0(call, _, _, state, ccc, _, _, ap, apa, _, ret, innerSummaryCtx, - innerArgApa) + fwdFlowThrough0(call, _, _, state, ccc, _, _, ap, _, _, ret, innerSummaryCtx) } pragma[nomagic] private predicate returnFlowsThrough( RetNodeEx ret, ReturnPosition pos, FlowState state, CcCall ccc, ParamNodeEx p, Typ argT, - Ap argAp, ApApprox argApa, TypOption argStored, Ap ap + Ap argAp, TypOption argStored, Ap ap ) { exists(DataFlowCall call, boolean allowsFieldFlow | - returnFlowsThrough0(call, state, ccc, ap, _, ret, - TSummaryCtxSome(p, _, argT, argAp, argStored), argApa) and + returnFlowsThrough0(call, state, ccc, ap, ret, + TSummaryCtxSome(p, _, argT, argAp, argStored)) and flowThroughOutOfCall(call, ccc, ret, _, allowsFieldFlow) and pos = ret.getReturnPosition() and if allowsFieldFlow = false then ap instanceof ApNil else any() @@ -2168,7 +2166,7 @@ module MakeImpl Lang> { ) { exists(Typ argT, TypOption argStored, boolean emptyArgAp | returnFlowsThrough(_, _, _, _, pragma[only_bind_into](p), pragma[only_bind_into](argT), - pragma[only_bind_into](argAp), _, pragma[only_bind_into](argStored), ap) and + pragma[only_bind_into](argAp), pragma[only_bind_into](argStored), ap) and flowIntoCallApaTaken(call, _, pragma[only_bind_into](arg), p, emptyArgAp) and fwdFlow(arg, _, _, _, pragma[only_bind_into](argT), pragma[only_bind_into](argAp), _, pragma[only_bind_into](argStored)) and @@ -2274,7 +2272,7 @@ module MakeImpl Lang> { // flow out of a callable exists(ReturnPosition pos | revFlowOut(_, node, pos, state, _, _, _, ap) and - if returnFlowsThrough(node, pos, state, _, _, _, _, _, _, ap) + if returnFlowsThrough(node, pos, state, _, _, _, _, _, ap) then ( returnCtx = TReturnCtxMaybeFlowThrough(pos) and returnAp = apSome(ap) @@ -2439,7 +2437,7 @@ module MakeImpl Lang> { ) { exists(RetNodeEx ret, FlowState state, CcCall ccc | revFlowOut(call, ret, pos, state, returnCtx, _, returnAp, ap) and - returnFlowsThrough(ret, pos, state, ccc, _, _, _, _, _, ap) and + returnFlowsThrough(ret, pos, state, ccc, _, _, _, _, ap) and matchesCall(ccc, call) ) } @@ -2508,7 +2506,7 @@ module MakeImpl Lang> { pragma[nomagic] private predicate parameterMayFlowThroughAp(ParamNodeEx p, Ap ap) { exists(ReturnPosition pos | - returnFlowsThrough(_, pos, _, _, p, _, ap, _, _, _) and + returnFlowsThrough(_, pos, _, _, p, _, ap, _, _) and parameterFlowsThroughRev(p, ap, pos, _) ) } @@ -2545,7 +2543,7 @@ module MakeImpl Lang> { pragma[nomagic] predicate returnMayFlowThrough(RetNodeEx ret, ReturnKindExt kind) { exists(ParamNodeEx p, ReturnPosition pos, Ap argAp, Ap ap | - returnFlowsThrough(ret, pos, _, _, p, _, argAp, _, _, ap) and + returnFlowsThrough(ret, pos, _, _, p, _, argAp, _, ap) and parameterFlowsThroughRev(p, argAp, pos, ap) and kind = pos.getKind() ) @@ -3133,11 +3131,11 @@ module MakeImpl Lang> { pragma[nomagic] private predicate fwdFlowThroughStep0( DataFlowCall call, ArgNodeEx arg, Cc cc, FlowState state, CcCall ccc, - SummaryCtx summaryCtx, Typ t, Ap ap, ApApprox apa, TypOption stored, RetNodeEx ret, + SummaryCtx summaryCtx, Typ t, Ap ap, TypOption stored, RetNodeEx ret, SummaryCtxSome innerSummaryCtx ) { - fwdFlowThrough0(call, arg, cc, state, ccc, summaryCtx, t, ap, apa, stored, ret, - innerSummaryCtx, _) + fwdFlowThrough0(call, arg, cc, state, ccc, summaryCtx, t, ap, _, stored, ret, + innerSummaryCtx) } bindingset[node, state, cc, summaryCtx, t, ap, stored] @@ -3162,14 +3160,14 @@ module MakeImpl Lang> { pragma[nomagic] private predicate fwdFlowThroughStep1( PathNodeImpl pn1, PathNodeImpl pn2, PathNodeImpl pn3, DataFlowCall call, Cc cc, - FlowState state, CcCall ccc, SummaryCtx summaryCtx, Typ t, Ap ap, ApApprox apa, - TypOption stored, RetNodeEx ret + FlowState state, CcCall ccc, SummaryCtx summaryCtx, Typ t, Ap ap, TypOption stored, + RetNodeEx ret ) { exists( FlowState state0, ArgNodeEx arg, SummaryCtxSome innerSummaryCtx, ParamNodeEx p, Typ innerArgT, Ap innerArgAp, TypOption innerArgStored | - fwdFlowThroughStep0(call, arg, cc, state, ccc, summaryCtx, t, ap, apa, stored, ret, + fwdFlowThroughStep0(call, arg, cc, state, ccc, summaryCtx, t, ap, stored, ret, innerSummaryCtx) and innerSummaryCtx = TSummaryCtxSome(p, state0, innerArgT, innerArgAp, innerArgStored) and pn1 = mkPathNode(arg, state0, cc, summaryCtx, innerArgT, innerArgAp, innerArgStored) and @@ -3186,7 +3184,7 @@ module MakeImpl Lang> { FlowState state, SummaryCtx summaryCtx, Typ t, Ap ap, TypOption stored ) { exists(DataFlowCall call, CcCall ccc, RetNodeEx ret, boolean allowsFieldFlow | - fwdFlowThroughStep1(pn1, pn2, pn3, call, cc, state, ccc, summaryCtx, t, ap, _, stored, + fwdFlowThroughStep1(pn1, pn2, pn3, call, cc, state, ccc, summaryCtx, t, ap, stored, ret) and flowThroughOutOfCall(call, ccc, ret, node, allowsFieldFlow) and not inBarrier(node, state) and From 22e0636cbad63262545f392b5f53f6ca64b74ce2 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 10 Dec 2024 13:06:29 +0100 Subject: [PATCH 07/14] Dataflow: Insert a few getApprox calls to remove even more columns. --- .../codeql/dataflow/internal/DataFlowImpl.qll | 58 +++++++++---------- 1 file changed, 29 insertions(+), 29 deletions(-) diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll index 6b24db3ea0c5..64630390fec5 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll @@ -1545,7 +1545,8 @@ module MakeImpl Lang> { apa = getApprox(ap) or // flow into a callable without summary context - fwdFlowInNoFlowThrough(node, apa, state, cc, t, ap, stored) and + fwdFlowInNoFlowThrough(node, state, cc, t, ap, stored) and + apa = getApprox(ap) and summaryCtx = TSummaryCtxNone() and // When the call contexts of source and sink needs to match then there's // never any reason to enter a callable except to find a summary. See also @@ -1553,7 +1554,8 @@ module MakeImpl Lang> { not Config::getAFeature() instanceof FeatureEqualSourceSinkCallContext or // flow into a callable with summary context (non-linear recursion) - fwdFlowInFlowThrough(node, apa, state, cc, t, ap, stored) and + fwdFlowInFlowThrough(node, state, cc, t, ap, stored) and + apa = getApprox(ap) and summaryCtx = TSummaryCtxSome(node, state, t, ap, stored) or // flow out of a callable @@ -1562,8 +1564,9 @@ module MakeImpl Lang> { or // flow through a callable exists(DataFlowCall call, CcCall ccc, RetNodeEx ret, boolean allowsFieldFlow | - fwdFlowThrough(call, cc, state, ccc, summaryCtx, t, ap, apa, stored, ret) and + fwdFlowThrough(call, cc, state, ccc, summaryCtx, t, ap, stored, ret) and flowThroughOutOfCall(call, ccc, ret, node, allowsFieldFlow) and + apa = getApprox(ap) and not inBarrier(node, state) and if allowsFieldFlow = false then ap instanceof ApNil else any() ) @@ -1572,7 +1575,7 @@ module MakeImpl Lang> { private newtype TSummaryCtx = TSummaryCtxNone() or TSummaryCtxSome(ParamNodeEx p, FlowState state, Typ t, Ap ap, TypOption stored) { - fwdFlowInFlowThrough(p, _, state, _, t, ap, stored) + fwdFlowInFlowThrough(p, state, _, t, ap, stored) } /** @@ -1823,11 +1826,10 @@ module MakeImpl Lang> { pragma[inline] private predicate fwdFlowInCandTypeFlowDisabled( DataFlowCall call, ArgNodeEx arg, FlowState state, Cc outercc, DataFlowCallable inner, - ParamNodeEx p, SummaryCtx summaryCtx, Typ t, Ap ap, ApApprox apa, TypOption stored, - boolean cc + ParamNodeEx p, SummaryCtx summaryCtx, Typ t, Ap ap, TypOption stored, boolean cc ) { not enableTypeFlow() and - fwdFlowInCand(call, arg, state, outercc, inner, p, summaryCtx, t, ap, _, apa, stored, cc) + fwdFlowInCand(call, arg, state, outercc, inner, p, summaryCtx, t, ap, _, _, stored, cc) } pragma[nomagic] @@ -1862,15 +1864,15 @@ module MakeImpl Lang> { predicate fwdFlowIn( DataFlowCall call, ArgNodeEx arg, DataFlowCallable inner, ParamNodeEx p, FlowState state, Cc outercc, CcCall innercc, SummaryCtx summaryCtx, Typ t, Ap ap, - ApApprox apa, TypOption stored, boolean cc + TypOption stored, boolean cc ) { // type flow disabled: linear recursion fwdFlowInCandTypeFlowDisabled(call, arg, state, outercc, inner, p, summaryCtx, t, ap, - apa, stored, cc) and + stored, cc) and fwdFlowInValidEdgeTypeFlowDisabled(call, inner, innercc, pragma[only_bind_into](cc)) or // type flow enabled: non-linear recursion - exists(boolean emptyAp | + exists(boolean emptyAp, ApApprox apa | fwdFlowIntoArg(arg, state, outercc, summaryCtx, t, ap, emptyAp, apa, stored, cc) and fwdFlowInValidEdgeTypeFlowEnabled(call, arg, outercc, inner, p, innercc, emptyAp, apa, cc) @@ -1884,10 +1886,9 @@ module MakeImpl Lang> { pragma[nomagic] private predicate fwdFlowInNoFlowThrough( - ParamNodeEx p, ApApprox apa, FlowState state, CcCall innercc, Typ t, Ap ap, - TypOption stored + ParamNodeEx p, FlowState state, CcCall innercc, Typ t, Ap ap, TypOption stored ) { - FwdFlowInNoThrough::fwdFlowIn(_, _, _, p, state, _, innercc, _, t, ap, apa, stored, _) + FwdFlowInNoThrough::fwdFlowIn(_, _, _, p, state, _, innercc, _, t, ap, stored, _) } private predicate top() { any() } @@ -1896,10 +1897,9 @@ module MakeImpl Lang> { pragma[nomagic] private predicate fwdFlowInFlowThrough( - ParamNodeEx p, ApApprox apa, FlowState state, CcCall innercc, Typ t, Ap ap, - TypOption stored + ParamNodeEx p, FlowState state, CcCall innercc, Typ t, Ap ap, TypOption stored ) { - FwdFlowInThrough::fwdFlowIn(_, _, _, p, state, _, innercc, _, t, ap, apa, stored, _) + FwdFlowInThrough::fwdFlowIn(_, _, _, p, state, _, innercc, _, t, ap, stored, _) } pragma[nomagic] @@ -1997,9 +1997,9 @@ module MakeImpl Lang> { DataFlowCall call, DataFlowCallable c, ParamNodeEx p, FlowState state, CcCall innercc, Typ t, Ap ap, TypOption stored, boolean cc ) { - FwdFlowInNoThrough::fwdFlowIn(call, _, c, p, state, _, innercc, _, t, ap, _, stored, cc) + FwdFlowInNoThrough::fwdFlowIn(call, _, c, p, state, _, innercc, _, t, ap, stored, cc) or - FwdFlowInThrough::fwdFlowIn(call, _, c, p, state, _, innercc, _, t, ap, _, stored, cc) + FwdFlowInThrough::fwdFlowIn(call, _, c, p, state, _, innercc, _, t, ap, stored, cc) } pragma[nomagic] @@ -2070,11 +2070,11 @@ module MakeImpl Lang> { pragma[nomagic] private predicate fwdFlowRetFromArg( RetNodeEx ret, FlowState state, CcCall ccc, SummaryCtxSome summaryCtx, Typ t, Ap ap, - ApApprox apa, TypOption stored + TypOption stored ) { exists(ReturnKindExt kind, ParamNodeEx p, Ap argAp | instanceofCcCall(ccc) and - fwdFlow(pragma[only_bind_into](ret), state, ccc, summaryCtx, t, ap, apa, stored) and + fwdFlow(pragma[only_bind_into](ret), state, ccc, summaryCtx, t, ap, _, stored) and summaryCtx = TSummaryCtxSome(pragma[only_bind_into](p), _, _, pragma[only_bind_into](argAp), _) and not outBarrier(ret, state) and @@ -2087,19 +2087,19 @@ module MakeImpl Lang> { pragma[inline] private predicate fwdFlowThrough0( DataFlowCall call, ArgNodeEx arg, Cc cc, FlowState state, CcCall ccc, - SummaryCtx summaryCtx, Typ t, Ap ap, ApApprox apa, TypOption stored, RetNodeEx ret, + SummaryCtx summaryCtx, Typ t, Ap ap, TypOption stored, RetNodeEx ret, SummaryCtxSome innerSummaryCtx ) { - fwdFlowRetFromArg(ret, state, ccc, innerSummaryCtx, t, ap, apa, stored) and + fwdFlowRetFromArg(ret, state, ccc, innerSummaryCtx, t, ap, stored) and fwdFlowIsEntered(call, arg, cc, ccc, summaryCtx, innerSummaryCtx) } pragma[nomagic] private predicate fwdFlowThrough( DataFlowCall call, Cc cc, FlowState state, CcCall ccc, SummaryCtx summaryCtx, Typ t, - Ap ap, ApApprox apa, TypOption stored, RetNodeEx ret + Ap ap, TypOption stored, RetNodeEx ret ) { - fwdFlowThrough0(call, _, cc, state, ccc, summaryCtx, t, ap, apa, stored, ret, _) + fwdFlowThrough0(call, _, cc, state, ccc, summaryCtx, t, ap, stored, ret, _) } pragma[nomagic] @@ -2107,7 +2107,7 @@ module MakeImpl Lang> { DataFlowCall call, ArgNodeEx arg, Cc cc, CcCall innerCc, SummaryCtx summaryCtx, ParamNodeEx p, FlowState state, Typ t, Ap ap, TypOption stored ) { - FwdFlowInThrough::fwdFlowIn(call, arg, _, p, state, cc, innerCc, summaryCtx, t, ap, _, + FwdFlowInThrough::fwdFlowIn(call, arg, _, p, state, cc, innerCc, summaryCtx, t, ap, stored, _) } @@ -2143,7 +2143,7 @@ module MakeImpl Lang> { DataFlowCall call, FlowState state, CcCall ccc, Ap ap, RetNodeEx ret, SummaryCtxSome innerSummaryCtx ) { - fwdFlowThrough0(call, _, _, state, ccc, _, _, ap, _, _, ret, innerSummaryCtx) + fwdFlowThrough0(call, _, _, state, ccc, _, _, ap, _, ret, innerSummaryCtx) } pragma[nomagic] @@ -3120,11 +3120,11 @@ module MakeImpl Lang> { SummaryCtx outerSummaryCtx, SummaryCtx innerSummaryCtx, Typ t, Ap ap, TypOption stored ) { FwdFlowInNoThrough::fwdFlowIn(_, arg, _, p, state, outercc, innercc, outerSummaryCtx, t, - ap, _, stored, _) and + ap, stored, _) and innerSummaryCtx = TSummaryCtxNone() or FwdFlowInThrough::fwdFlowIn(_, arg, _, p, state, outercc, innercc, outerSummaryCtx, t, - ap, _, stored, _) and + ap, stored, _) and innerSummaryCtx = TSummaryCtxSome(p, state, t, ap, stored) } @@ -3134,7 +3134,7 @@ module MakeImpl Lang> { SummaryCtx summaryCtx, Typ t, Ap ap, TypOption stored, RetNodeEx ret, SummaryCtxSome innerSummaryCtx ) { - fwdFlowThrough0(call, arg, cc, state, ccc, summaryCtx, t, ap, _, stored, ret, + fwdFlowThrough0(call, arg, cc, state, ccc, summaryCtx, t, ap, stored, ret, innerSummaryCtx) } From 501cbdab3c4e5bdbd6e417d4e5e369dfcfcb3657 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 10 Dec 2024 13:12:32 +0100 Subject: [PATCH 08/14] Dataflow: Remove another ApApprox join and related columns. --- .../codeql/dataflow/internal/DataFlowImpl.qll | 27 +++++++++---------- 1 file changed, 13 insertions(+), 14 deletions(-) diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll index 64630390fec5..20ead18e692b 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll @@ -1717,9 +1717,9 @@ module MakeImpl Lang> { pragma[nomagic] private predicate fwdFlowIntoArg( ArgNodeEx arg, FlowState state, Cc outercc, SummaryCtx summaryCtx, Typ t, Ap ap, - boolean emptyAp, ApApprox apa, TypOption stored, boolean cc + boolean emptyAp, TypOption stored, boolean cc ) { - fwdFlow(arg, state, outercc, summaryCtx, t, ap, apa, stored) and + fwdFlow(arg, state, outercc, summaryCtx, t, ap, _, stored) and (if instanceofCcCall(outercc) then cc = true else cc = false) and if ap instanceof ApNil then emptyAp = true else emptyAp = false } @@ -1809,10 +1809,10 @@ module MakeImpl Lang> { pragma[inline] private predicate fwdFlowInCand( DataFlowCall call, ArgNodeEx arg, FlowState state, Cc outercc, DataFlowCallable inner, - ParamNodeEx p, SummaryCtx summaryCtx, Typ t, Ap ap, boolean emptyAp, ApApprox apa, - TypOption stored, boolean cc + ParamNodeEx p, SummaryCtx summaryCtx, Typ t, Ap ap, boolean emptyAp, TypOption stored, + boolean cc ) { - fwdFlowIntoArg(arg, state, outercc, summaryCtx, t, ap, emptyAp, apa, stored, cc) and + fwdFlowIntoArg(arg, state, outercc, summaryCtx, t, ap, emptyAp, stored, cc) and ( inner = viableImplCallContextReducedInlineLate(call, arg, outercc) or @@ -1829,16 +1829,16 @@ module MakeImpl Lang> { ParamNodeEx p, SummaryCtx summaryCtx, Typ t, Ap ap, TypOption stored, boolean cc ) { not enableTypeFlow() and - fwdFlowInCand(call, arg, state, outercc, inner, p, summaryCtx, t, ap, _, _, stored, cc) + fwdFlowInCand(call, arg, state, outercc, inner, p, summaryCtx, t, ap, _, stored, cc) } pragma[nomagic] private predicate fwdFlowInCandTypeFlowEnabled( DataFlowCall call, ArgNodeEx arg, Cc outercc, DataFlowCallable inner, ParamNodeEx p, - boolean emptyAp, ApApprox apa, boolean cc + boolean emptyAp, boolean cc ) { enableTypeFlow() and - fwdFlowInCand(call, arg, _, outercc, inner, p, _, _, _, emptyAp, apa, _, cc) + fwdFlowInCand(call, arg, _, outercc, inner, p, _, _, _, emptyAp, _, cc) } pragma[nomagic] @@ -1853,9 +1853,9 @@ module MakeImpl Lang> { pragma[nomagic] private predicate fwdFlowInValidEdgeTypeFlowEnabled( DataFlowCall call, ArgNodeEx arg, Cc outercc, DataFlowCallable inner, ParamNodeEx p, - CcCall innercc, boolean emptyAp, ApApprox apa, boolean cc + CcCall innercc, boolean emptyAp, boolean cc ) { - fwdFlowInCandTypeFlowEnabled(call, arg, outercc, inner, p, emptyAp, apa, cc) and + fwdFlowInCandTypeFlowEnabled(call, arg, outercc, inner, p, emptyAp, cc) and FwdTypeFlow::typeFlowValidEdgeIn(call, inner, cc) and innercc = getCallContextCall(call, inner) } @@ -1872,10 +1872,9 @@ module MakeImpl Lang> { fwdFlowInValidEdgeTypeFlowDisabled(call, inner, innercc, pragma[only_bind_into](cc)) or // type flow enabled: non-linear recursion - exists(boolean emptyAp, ApApprox apa | - fwdFlowIntoArg(arg, state, outercc, summaryCtx, t, ap, emptyAp, apa, stored, cc) and - fwdFlowInValidEdgeTypeFlowEnabled(call, arg, outercc, inner, p, innercc, emptyAp, apa, - cc) + exists(boolean emptyAp | + fwdFlowIntoArg(arg, state, outercc, summaryCtx, t, ap, emptyAp, stored, cc) and + fwdFlowInValidEdgeTypeFlowEnabled(call, arg, outercc, inner, p, innercc, emptyAp, cc) ) } } From 231bf9d1c9e0fdf0c30300112501fe8a882a5591 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 10 Dec 2024 13:20:27 +0100 Subject: [PATCH 09/14] Dataflow: Drop ApApprox join in fwdFlowStore. --- .../codeql/dataflow/internal/DataFlowImpl.qll | 31 +++++++++---------- 1 file changed, 14 insertions(+), 17 deletions(-) diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll index 20ead18e692b..426c6200e907 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll @@ -877,13 +877,11 @@ module MakeImpl Lang> { pragma[nomagic] predicate storeStepCand( - NodeEx node1, Ap ap1, Content c, NodeEx node2, DataFlowType contentType, - DataFlowType containerType + NodeEx node1, Content c, NodeEx node2, DataFlowType contentType, DataFlowType containerType ) { revFlowIsReadAndStored(c) and revFlow(node2) and - store(node1, c, node2, contentType, containerType) and - exists(ap1) + store(node1, c, node2, contentType, containerType) } pragma[nomagic] @@ -1292,8 +1290,7 @@ module MakeImpl Lang> { predicate returnMayFlowThrough(RetNodeEx ret, ReturnKindExt kind); predicate storeStepCand( - NodeEx node1, Ap ap1, Content c, NodeEx node2, DataFlowType contentType, - DataFlowType containerType + NodeEx node1, Content c, NodeEx node2, DataFlowType contentType, DataFlowType containerType ); predicate readStepCand(NodeEx n1, Content c, NodeEx n2); @@ -1451,7 +1448,7 @@ module MakeImpl Lang> { pragma[nomagic] private predicate compatibleContainer0(ApHeadContent apc, DataFlowType containerType) { exists(DataFlowType containerType0, Content c | - PrevStage::storeStepCand(_, _, c, _, _, containerType0) and + PrevStage::storeStepCand(_, c, _, _, containerType0) and not isTopType(containerType0) and compatibleTypesCached(containerType0, containerType) and apc = projectToHeadContent(c) @@ -1461,7 +1458,7 @@ module MakeImpl Lang> { pragma[nomagic] private predicate topTypeContent(ApHeadContent apc) { exists(DataFlowType containerType0, Content c | - PrevStage::storeStepCand(_, _, c, _, _, containerType0) and + PrevStage::storeStepCand(_, c, _, _, containerType0) and isTopType(containerType0) and apc = projectToHeadContent(c) ) @@ -1646,11 +1643,11 @@ module MakeImpl Lang> { NodeEx node1, Typ t1, Ap ap1, TypOption stored1, Content c, Typ t2, TypOption stored2, NodeEx node2, FlowState state, Cc cc, SummaryCtx summaryCtx ) { - exists(DataFlowType contentType, DataFlowType containerType, ApApprox apa1 | - fwdFlow(node1, state, cc, summaryCtx, t1, ap1, apa1, stored1) and + exists(DataFlowType contentType, DataFlowType containerType | + fwdFlow(node1, state, cc, summaryCtx, t1, ap1, _, stored1) and not outBarrier(node1, state) and not inBarrier(node2, state) and - PrevStage::storeStepCand(node1, apa1, c, node2, contentType, containerType) and + PrevStage::storeStepCand(node1, c, node2, contentType, containerType) and t2 = getTyp(containerType) and // We need to typecheck stores here, since reverse flow through a getter // might have a different type here compared to inside the getter. @@ -2443,11 +2440,11 @@ module MakeImpl Lang> { pragma[nomagic] predicate storeStepCand( - NodeEx node1, Ap ap1, Content c, NodeEx node2, DataFlowType contentType, + NodeEx node1, Content c, NodeEx node2, DataFlowType contentType, DataFlowType containerType ) { - exists(Ap ap2 | - PrevStage::storeStepCand(node1, _, c, node2, contentType, containerType) and + exists(Ap ap2, Ap ap1 | + PrevStage::storeStepCand(node1, c, node2, contentType, containerType) and revFlowStore(ap2, c, ap1, node1, _, node2, _, _) and revFlowConsCand(ap2, c, ap1) ) @@ -2664,7 +2661,7 @@ module MakeImpl Lang> { or node instanceof OutNodeEx or - storeStepCand(_, _, _, node, _, _) + storeStepCand(_, _, node, _, _) or readStepCand(_, _, node) or @@ -2698,7 +2695,7 @@ module MakeImpl Lang> { callEdgeReturn(_, _, node, _, next, _) and apNext = ap or - storeStepCand(node, _, _, next, _, _) + storeStepCand(node, _, next, _, _) or readStepCand(node, _, next) ) @@ -3950,7 +3947,7 @@ module MakeImpl Lang> { PrevStage::readStepCand(_, pragma[only_bind_into](c), _) and c = cs.getAReadContent() and clearSet(node, cs) and - if PrevStage::storeStepCand(_, _, _, node, _, _) + if PrevStage::storeStepCand(_, _, node, _, _) then isStoreTarget = true else isStoreTarget = false ) From 4e155f8542c4dcfb4216d078c34e6f69fabd52f5 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 10 Dec 2024 13:23:51 +0100 Subject: [PATCH 10/14] Dataflow: Insert a few getApprox calls to remove ApApprox from fwdFlow. --- .../codeql/dataflow/internal/DataFlowImpl.qll | 85 ++++++++++--------- 1 file changed, 43 insertions(+), 42 deletions(-) diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll index 426c6200e907..56bf55307042 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll @@ -1479,26 +1479,27 @@ module MakeImpl Lang> { */ pragma[nomagic] additional predicate fwdFlow( - NodeEx node, FlowState state, Cc cc, SummaryCtx summaryCtx, Typ t, Ap ap, ApApprox apa, - TypOption stored + NodeEx node, FlowState state, Cc cc, SummaryCtx summaryCtx, Typ t, Ap ap, TypOption stored ) { - fwdFlow1(node, state, cc, summaryCtx, _, t, ap, apa, stored) + fwdFlow1(node, state, cc, summaryCtx, _, t, ap, stored) } private predicate fwdFlow1( NodeEx node, FlowState state, Cc cc, SummaryCtx summaryCtx, Typ t0, Typ t, Ap ap, - ApApprox apa, TypOption stored + TypOption stored ) { - fwdFlow0(node, state, cc, summaryCtx, t0, ap, apa, stored) and - PrevStage::revFlow(node, state, apa) and - filter(node, state, t0, ap, t) and - ( - if node instanceof CastingNodeEx - then - ap instanceof ApNil or - compatibleContainer(getHeadContent(ap), node.getDataFlowType()) or - topTypeContent(getHeadContent(ap)) - else any() + exists(ApApprox apa | + fwdFlow0(node, state, cc, summaryCtx, t0, ap, apa, stored) and + PrevStage::revFlow(node, state, apa) and + filter(node, state, t0, ap, t) and + ( + if node instanceof CastingNodeEx + then + ap instanceof ApNil or + compatibleContainer(getHeadContent(ap), node.getDataFlowType()) or + topTypeContent(getHeadContent(ap)) + else any() + ) ) } @@ -1516,7 +1517,8 @@ module MakeImpl Lang> { stored.isNone() or exists(NodeEx mid, FlowState state0, Typ t0, LocalCc localCc | - fwdFlow(mid, state0, cc, summaryCtx, t0, ap, apa, stored) and + fwdFlow(mid, state0, cc, summaryCtx, t0, ap, stored) and + apa = getApprox(ap) and localCc = getLocalCc(cc) | localStep(mid, state0, node, state, true, _, localCc, _) and @@ -1526,7 +1528,8 @@ module MakeImpl Lang> { ap instanceof ApNil ) or - fwdFlowJump(node, state, t, ap, apa, stored) and + fwdFlowJump(node, state, t, ap, stored) and + apa = getApprox(ap) and cc = ccNone() and summaryCtx = TSummaryCtxNone() or @@ -1615,23 +1618,21 @@ module MakeImpl Lang> { override Location getLocation() { result = p.getLocation() } } - private predicate fwdFlowJump( - NodeEx node, FlowState state, Typ t, Ap ap, ApApprox apa, TypOption stored - ) { + private predicate fwdFlowJump(NodeEx node, FlowState state, Typ t, Ap ap, TypOption stored) { exists(NodeEx mid | - fwdFlow(mid, state, _, _, t, ap, apa, stored) and + fwdFlow(mid, state, _, _, t, ap, stored) and jumpStepEx(mid, node) ) or exists(NodeEx mid | - fwdFlow(mid, state, _, _, _, ap, apa, stored) and + fwdFlow(mid, state, _, _, _, ap, stored) and additionalJumpStep(mid, node, _) and t = getNodeTyp(node) and ap instanceof ApNil ) or exists(NodeEx mid, FlowState state0 | - fwdFlow(mid, state0, _, _, _, ap, apa, stored) and + fwdFlow(mid, state0, _, _, _, ap, stored) and additionalJumpStateStep(mid, state0, node, state, _) and t = getNodeTyp(node) and ap instanceof ApNil @@ -1644,7 +1645,7 @@ module MakeImpl Lang> { NodeEx node2, FlowState state, Cc cc, SummaryCtx summaryCtx ) { exists(DataFlowType contentType, DataFlowType containerType | - fwdFlow(node1, state, cc, summaryCtx, t1, ap1, _, stored1) and + fwdFlow(node1, state, cc, summaryCtx, t1, ap1, stored1) and not outBarrier(node1, state) and not inBarrier(node2, state) and PrevStage::storeStepCand(node1, c, node2, contentType, containerType) and @@ -1685,7 +1686,7 @@ module MakeImpl Lang> { Cc cc, SummaryCtx summaryCtx ) { exists(ApHeadContent apc | - fwdFlow(node1, state, cc, summaryCtx, t, ap, _, stored) and + fwdFlow(node1, state, cc, summaryCtx, t, ap, stored) and not outBarrier(node1, state) and not inBarrier(node2, state) and apc = getHeadContent(ap) and @@ -1716,7 +1717,7 @@ module MakeImpl Lang> { ArgNodeEx arg, FlowState state, Cc outercc, SummaryCtx summaryCtx, Typ t, Ap ap, boolean emptyAp, TypOption stored, boolean cc ) { - fwdFlow(arg, state, outercc, summaryCtx, t, ap, _, stored) and + fwdFlow(arg, state, outercc, summaryCtx, t, ap, stored) and (if instanceofCcCall(outercc) then cc = true else cc = false) and if ap instanceof ApNil then emptyAp = true else emptyAp = false } @@ -1940,7 +1941,7 @@ module MakeImpl Lang> { ) { instanceofCcNoCall(cc) and not outBarrier(ret, state) and - fwdFlow(ret, state, cc, summaryCtx, t, ap, _, stored) + fwdFlow(ret, state, cc, summaryCtx, t, ap, stored) } pragma[nomagic] @@ -2003,7 +2004,7 @@ module MakeImpl Lang> { ParamNodeEx p, FlowState state, CcCall cc, Typ t0, Ap ap, TypOption stored ) { instanceofCcCall(cc) and - fwdFlow1(p, state, cc, _, t0, _, ap, _, stored) + fwdFlow1(p, state, cc, _, t0, _, ap, stored) } pragma[nomagic] @@ -2026,7 +2027,7 @@ module MakeImpl Lang> { private predicate fwdFlow1Out( NodeEx node, FlowState state, Cc cc, Typ t0, Ap ap, TypOption stored ) { - fwdFlow1(node, state, cc, _, t0, _, ap, _, stored) and + fwdFlow1(node, state, cc, _, t0, _, ap, stored) and PrevStage::callEdgeReturn(_, _, _, _, node, _) } @@ -2048,7 +2049,7 @@ module MakeImpl Lang> { or exists(NodeEx node | cc = false and - fwdFlowJump(node, _, _, _, _, _) and + fwdFlowJump(node, _, _, _, _) and c = node.getEnclosingCallable() ) } @@ -2070,7 +2071,7 @@ module MakeImpl Lang> { ) { exists(ReturnKindExt kind, ParamNodeEx p, Ap argAp | instanceofCcCall(ccc) and - fwdFlow(pragma[only_bind_into](ret), state, ccc, summaryCtx, t, ap, _, stored) and + fwdFlow(pragma[only_bind_into](ret), state, ccc, summaryCtx, t, ap, stored) and summaryCtx = TSummaryCtxSome(pragma[only_bind_into](p), _, _, pragma[only_bind_into](argAp), _) and not outBarrier(ret, state) and @@ -2164,7 +2165,7 @@ module MakeImpl Lang> { returnFlowsThrough(_, _, _, _, pragma[only_bind_into](p), pragma[only_bind_into](argT), pragma[only_bind_into](argAp), pragma[only_bind_into](argStored), ap) and flowIntoCallApaTaken(call, _, pragma[only_bind_into](arg), p, emptyArgAp) and - fwdFlow(arg, _, _, _, pragma[only_bind_into](argT), pragma[only_bind_into](argAp), _, + fwdFlow(arg, _, _, _, pragma[only_bind_into](argT), pragma[only_bind_into](argAp), pragma[only_bind_into](argStored)) and if argAp instanceof ApNil then emptyArgAp = true else emptyArgAp = false ) @@ -2176,7 +2177,7 @@ module MakeImpl Lang> { ) { exists(boolean emptyAp | flowIntoCallApaTaken(call, c, arg, p, emptyAp) and - fwdFlow(arg, _, _, _, _, ap, _, _) and + fwdFlow(arg, _, _, _, _, ap, _) and if ap instanceof ApNil then emptyAp = true else emptyAp = false ) } @@ -2187,7 +2188,7 @@ module MakeImpl Lang> { Ap ap, boolean allowsFieldFlow ) { PrevStage::callEdgeReturn(call, c, ret, _, out, allowsFieldFlow) and - fwdFlow(ret, _, _, _, _, ap, _, _) and + fwdFlow(ret, _, _, _, _, ap, _) and pos = ret.getReturnPosition() and (if allowsFieldFlow = false then ap instanceof ApNil else any()) and ( @@ -2210,14 +2211,14 @@ module MakeImpl Lang> { NodeEx node, FlowState state, ReturnCtx returnCtx, ApOption returnAp, Ap ap ) { revFlow0(node, state, returnCtx, returnAp, ap) and - fwdFlow(node, state, _, _, _, ap, _, _) + fwdFlow(node, state, _, _, _, ap, _) } pragma[nomagic] private predicate revFlow0( NodeEx node, FlowState state, ReturnCtx returnCtx, ApOption returnAp, Ap ap ) { - fwdFlow(node, state, _, _, _, ap, _, _) and + fwdFlow(node, state, _, _, _, ap, _) and sinkNode(node, state) and ( if hasSinkCallCtx() @@ -2345,7 +2346,7 @@ module MakeImpl Lang> { predicate dataFlowNonCallEntry(DataFlowCallable c, boolean cc) { exists(NodeEx node, FlowState state, ApNil nil | - fwdFlow(node, state, _, _, _, nil, _, _) and + fwdFlow(node, state, _, _, _, nil, _) and sinkNode(node, state) and (if hasSinkCallCtx() then cc = true else cc = false) and c = node.getEnclosingCallable() @@ -2520,7 +2521,7 @@ module MakeImpl Lang> { exists(Ap ap0 | parameterMayFlowThrough(p, _) and revFlow(n, state, TReturnCtxMaybeFlowThrough(_), _, ap0) and - fwdFlow(n, state, any(CcCall ccc), TSummaryCtxSome(p, _, _, ap, _), _, ap0, _, _) + fwdFlow(n, state, any(CcCall ccc), TSummaryCtxSome(p, _, _, ap, _), _, ap0, _) ) } @@ -2812,7 +2813,7 @@ module MakeImpl Lang> { NodeEx node, FlowState state, Cc cc, SummaryCtx summaryCtx, Typ t, Ap ap, TypOption stored ) { - fwdFlow(node, state, cc, summaryCtx, t, ap, _, stored) and + fwdFlow(node, state, cc, summaryCtx, t, ap, stored) and revFlow(node, state, _, _, ap) } or TPathNodeSink(NodeEx node, FlowState state) { @@ -3148,7 +3149,7 @@ module MakeImpl Lang> { TypOption stored ) { exists(Typ t | - fwdFlow1(node, state, cc, summaryCtx, t0, t, ap, _, stored) and + fwdFlow1(node, state, cc, summaryCtx, t0, t, ap, stored) and result = TPathNodeMid(node, state, cc, summaryCtx, t, ap, stored) ) } @@ -3598,13 +3599,13 @@ module MakeImpl Lang> { int tfnodes, int tftuples ) { fwd = true and - nodes = count(NodeEx node | fwdFlow(node, _, _, _, _, _, _, _)) and + nodes = count(NodeEx node | fwdFlow(node, _, _, _, _, _, _)) and fields = count(Content f0 | fwdConsCand(f0, _)) and conscand = count(Content f0, Ap ap | fwdConsCand(f0, ap)) and - states = count(FlowState state | fwdFlow(_, state, _, _, _, _, _, _)) and + states = count(FlowState state | fwdFlow(_, state, _, _, _, _, _)) and tuples = count(NodeEx n, FlowState state, Cc cc, SummaryCtx summaryCtx, Typ t, Ap ap, - TypOption stored | fwdFlow(n, state, cc, summaryCtx, t, ap, _, stored)) and + TypOption stored | fwdFlow(n, state, cc, summaryCtx, t, ap, stored)) and calledges = count(DataFlowCall call, DataFlowCallable c | FwdTypeFlowInput::dataFlowTakenCallEdgeIn(call, c, _) or From 40f77136787ab75491b604b9e6a7bfaa2b1f6f00 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 10 Dec 2024 13:28:43 +0100 Subject: [PATCH 11/14] Dataflow: Minor simplification. --- shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll index 56bf55307042..6ead5b719065 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll @@ -2043,7 +2043,7 @@ module MakeImpl Lang> { 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 + PrevStage::revFlow(node, state, any(PrevStage::ApNil nil)) and c = node.getEnclosingCallable() ) or From da179705c393598d6c15d57b5a266b397e3232ac Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 10 Dec 2024 14:52:06 +0100 Subject: [PATCH 12/14] Java: Accept expected file changes. --- .../test/library-tests/dataflow/capture/inlinetest.expected | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/java/ql/test/library-tests/dataflow/capture/inlinetest.expected b/java/ql/test/library-tests/dataflow/capture/inlinetest.expected index d127b92ddafa..a336577503f2 100644 --- a/java/ql/test/library-tests/dataflow/capture/inlinetest.expected +++ b/java/ql/test/library-tests/dataflow/capture/inlinetest.expected @@ -171,10 +171,12 @@ edges | B.java:154:17:154:28 | source(...) : String | B.java:175:5:175:6 | String s2 : String | provenance | | | B.java:158:7:158:13 | parameter this : MyLocal [String s1] : String | B.java:159:18:159:19 | this : MyLocal [String s1] : String | provenance | | | B.java:158:7:158:13 | parameter this : MyLocal [String s2] : String | B.java:160:14:160:15 | this : MyLocal [String s2] : String | provenance | | +| B.java:158:7:158:13 | parameter this : MyLocal [String s2] : String | B.java:160:14:160:15 | this : MyLocal [String s2] : String | provenance | | | B.java:159:9:159:12 | this [post update] : MyLocal [f] : String | B.java:158:7:158:13 | parameter this [Return] : MyLocal [f] : String | provenance | | | B.java:159:18:159:19 | s1 : String | B.java:159:9:159:12 | this [post update] : MyLocal [f] : String | provenance | | | B.java:159:18:159:19 | this : MyLocal [String s1] : String | B.java:159:18:159:19 | s1 : String | provenance | | | B.java:160:14:160:15 | this : MyLocal [String s2] : String | B.java:160:14:160:15 | s2 | provenance | | +| B.java:160:14:160:15 | this : MyLocal [String s2] : String | B.java:160:14:160:15 | s2 | provenance | | | B.java:162:12:162:15 | parameter this : MyLocal [String s2] : String | B.java:164:14:164:15 | this : MyLocal [String s2] : String | provenance | | | B.java:162:12:162:15 | parameter this : MyLocal [f] : String | B.java:163:14:163:14 | this <.field> : MyLocal [f] : String | provenance | | | B.java:163:14:163:14 | this <.field> : MyLocal [f] : String | B.java:163:14:163:14 | f | provenance | | @@ -464,12 +466,14 @@ nodes | B.java:154:17:154:28 | source(...) : String | semmle.label | source(...) : String | | B.java:158:7:158:13 | parameter this : MyLocal [String s1] : String | semmle.label | parameter this : MyLocal [String s1] : String | | B.java:158:7:158:13 | parameter this : MyLocal [String s2] : String | semmle.label | parameter this : MyLocal [String s2] : String | +| B.java:158:7:158:13 | parameter this : MyLocal [String s2] : String | semmle.label | parameter this : MyLocal [String s2] : String | | B.java:158:7:158:13 | parameter this [Return] : MyLocal [f] : String | semmle.label | parameter this [Return] : MyLocal [f] : String | | B.java:159:9:159:12 | this [post update] : MyLocal [f] : String | semmle.label | this [post update] : MyLocal [f] : String | | B.java:159:18:159:19 | s1 : String | semmle.label | s1 : String | | B.java:159:18:159:19 | this : MyLocal [String s1] : String | semmle.label | this : MyLocal [String s1] : String | | B.java:160:14:160:15 | s2 | semmle.label | s2 | | B.java:160:14:160:15 | this : MyLocal [String s2] : String | semmle.label | this : MyLocal [String s2] : String | +| B.java:160:14:160:15 | this : MyLocal [String s2] : String | semmle.label | this : MyLocal [String s2] : String | | B.java:162:12:162:15 | parameter this : MyLocal [String s2] : String | semmle.label | parameter this : MyLocal [String s2] : String | | B.java:162:12:162:15 | parameter this : MyLocal [f] : String | semmle.label | parameter this : MyLocal [f] : String | | B.java:163:14:163:14 | f | semmle.label | f | From d6a4080baf3ba978284576dcfddbcdf3d2bc20f7 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 11 Dec 2024 11:18:57 +0100 Subject: [PATCH 13/14] Dataflow: Address review comment. --- .../codeql/dataflow/internal/DataFlowImpl.qll | 36 +++++++++---------- 1 file changed, 17 insertions(+), 19 deletions(-) diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll index 6ead5b719065..622fff860b59 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll @@ -1427,6 +1427,11 @@ module MakeImpl Lang> { ) } + bindingset[ap] + private boolean isNil(Ap ap) { + if ap instanceof ApNil then result = true else result = false + } + /* Begin: Stage logic. */ pragma[nomagic] private Typ getNodeTyp(NodeEx node) { @@ -1719,7 +1724,7 @@ module MakeImpl Lang> { ) { fwdFlow(arg, state, outercc, summaryCtx, t, ap, stored) and (if instanceofCcCall(outercc) then cc = true else cc = false) and - if ap instanceof ApNil then emptyAp = true else emptyAp = false + emptyAp = isNil(ap) } private signature predicate flowThroughSig(); @@ -2161,13 +2166,12 @@ module MakeImpl Lang> { private predicate flowThroughIntoCall( DataFlowCall call, ArgNodeEx arg, ParamNodeEx p, Ap argAp, Ap ap ) { - exists(Typ argT, TypOption argStored, boolean emptyArgAp | + exists(Typ argT, TypOption argStored | returnFlowsThrough(_, _, _, _, pragma[only_bind_into](p), pragma[only_bind_into](argT), pragma[only_bind_into](argAp), pragma[only_bind_into](argStored), ap) and - flowIntoCallApaTaken(call, _, pragma[only_bind_into](arg), p, emptyArgAp) and + flowIntoCallApaTaken(call, _, pragma[only_bind_into](arg), p, isNil(argAp)) and fwdFlow(arg, _, _, _, pragma[only_bind_into](argT), pragma[only_bind_into](argAp), - pragma[only_bind_into](argStored)) and - if argAp instanceof ApNil then emptyArgAp = true else emptyArgAp = false + pragma[only_bind_into](argStored)) ) } @@ -2175,11 +2179,8 @@ module MakeImpl Lang> { private predicate flowIntoCallAp( DataFlowCall call, DataFlowCallable c, ArgNodeEx arg, ParamNodeEx p, Ap ap ) { - exists(boolean emptyAp | - flowIntoCallApaTaken(call, c, arg, p, emptyAp) and - fwdFlow(arg, _, _, _, _, ap, _) and - if ap instanceof ApNil then emptyAp = true else emptyAp = false - ) + flowIntoCallApaTaken(call, c, arg, p, isNil(ap)) and + fwdFlow(arg, _, _, _, _, ap, _) } pragma[nomagic] @@ -2405,13 +2406,10 @@ module MakeImpl Lang> { private predicate revFlowParamToReturn( ParamNodeEx p, FlowState state, ReturnPosition pos, Ap returnAp, Ap ap ) { - exists(boolean emptyAp | - revFlow(pragma[only_bind_into](p), state, TReturnCtxMaybeFlowThrough(pos), - apSome(returnAp), pragma[only_bind_into](ap)) and - parameterFlowThroughAllowed(p, pos.getKind()) and - PrevStage::parameterMayFlowThrough(p, emptyAp) and - if ap instanceof ApNil then emptyAp = true else emptyAp = false - ) + revFlow(pragma[only_bind_into](p), state, TReturnCtxMaybeFlowThrough(pos), + apSome(returnAp), pragma[only_bind_into](ap)) and + parameterFlowThroughAllowed(p, pos.getKind()) and + PrevStage::parameterMayFlowThrough(p, isNil(ap)) } pragma[nomagic] @@ -2512,7 +2510,7 @@ module MakeImpl Lang> { predicate parameterMayFlowThrough(ParamNodeEx p, boolean emptyAp) { exists(Ap ap | parameterMayFlowThroughAp(p, ap) and - if ap instanceof ApNil then emptyAp = true else emptyAp = false + emptyAp = isNil(ap) ) } @@ -2572,7 +2570,7 @@ module MakeImpl Lang> { flowIntoCallAp(call, c, arg, p, ap) and revFlow(arg, pragma[only_bind_into](state), pragma[only_bind_into](ap)) and revFlow(p, pragma[only_bind_into](state), pragma[only_bind_into](ap)) and - if ap instanceof ApNil then emptyAp = true else emptyAp = false + emptyAp = isNil(ap) | // both directions are needed for flow-through RevTypeFlowInput::dataFlowTakenCallEdgeIn(call, c, _) or From cac131df37f1edfc2dda9405a5c3c8879ac8be95 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 11 Dec 2024 11:22:42 +0100 Subject: [PATCH 14/14] Dataflow: Rename a couple of predicates. --- .../codeql/dataflow/internal/DataFlowImpl.qll | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll index 622fff860b59..e50efcb5532b 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll @@ -1922,7 +1922,7 @@ module MakeImpl Lang> { bindingset[call] pragma[inline_late] - private predicate flowOutOfCallApaInlineLate( + private predicate flowOutOfCallInlineLate( DataFlowCall call, DataFlowCallable c, RetNodeEx ret, NodeEx out, boolean allowsFieldFlow ) { PrevStage::callEdgeReturn(call, c, ret, _, out, allowsFieldFlow) @@ -1931,7 +1931,7 @@ module MakeImpl Lang> { bindingset[c, ret, innercc] pragma[inline_late] pragma[noopt] - private predicate flowOutOfCallApaNotCallContextReduced( + private predicate flowOutOfCallNotCallContextReduced( DataFlowCall call, DataFlowCallable c, RetNodeEx ret, NodeEx out, boolean allowsFieldFlow, CcNoCall innercc ) { @@ -1958,9 +1958,9 @@ module MakeImpl Lang> { inner = ret.getEnclosingCallable() and ( call = viableImplCallContextReducedReverseInlineLate(inner, innercc) and - flowOutOfCallApaInlineLate(call, inner, ret, out, allowsFieldFlow) + flowOutOfCallInlineLate(call, inner, ret, out, allowsFieldFlow) or - flowOutOfCallApaNotCallContextReduced(call, inner, ret, out, allowsFieldFlow, innercc) + flowOutOfCallNotCallContextReduced(call, inner, ret, out, allowsFieldFlow, innercc) ) } @@ -2062,7 +2062,7 @@ module MakeImpl Lang> { private module FwdTypeFlow = TypeFlow; - private predicate flowIntoCallApaTaken( + private predicate flowIntoCallTaken( DataFlowCall call, DataFlowCallable c, ArgNodeEx arg, ParamNodeEx p, boolean emptyAp ) { PrevStage::callEdgeArgParam(call, c, arg, p, emptyAp) and @@ -2169,7 +2169,7 @@ module MakeImpl Lang> { exists(Typ argT, TypOption argStored | returnFlowsThrough(_, _, _, _, pragma[only_bind_into](p), pragma[only_bind_into](argT), pragma[only_bind_into](argAp), pragma[only_bind_into](argStored), ap) and - flowIntoCallApaTaken(call, _, pragma[only_bind_into](arg), p, isNil(argAp)) and + flowIntoCallTaken(call, _, pragma[only_bind_into](arg), p, isNil(argAp)) and fwdFlow(arg, _, _, _, pragma[only_bind_into](argT), pragma[only_bind_into](argAp), pragma[only_bind_into](argStored)) ) @@ -2179,7 +2179,7 @@ module MakeImpl Lang> { private predicate flowIntoCallAp( DataFlowCall call, DataFlowCallable c, ArgNodeEx arg, ParamNodeEx p, Ap ap ) { - flowIntoCallApaTaken(call, c, arg, p, isNil(ap)) and + flowIntoCallTaken(call, c, arg, p, isNil(ap)) and fwdFlow(arg, _, _, _, _, ap, _) }