diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll index 23f3f0917f551..06ccf3700e09b 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll @@ -1719,7 +1719,8 @@ module MakeImpl Lang> { Typ t1, Ap ap1, Typ t2, Ap ap2, Content c, NodeEx node1, NodeEx node2, FlowState state, Cc cc, ParamNodeOption summaryCtx, TypOption argT, ApOption argAp ) { - fwdFlowRead0(t1, ap1, c, node1, node2, state, cc, summaryCtx, argT, argAp) and + fwdFlowRead0(pragma[only_bind_into](t1), pragma[only_bind_into](ap1), + pragma[only_bind_into](c), node1, node2, state, cc, summaryCtx, argT, argAp) and ( exists(NodeEx storeSource | fwdFlowConsCandStoreReadMatchingEnabled(storeSource, t1, ap1, c, t2, ap2) and @@ -2646,7 +2647,16 @@ module MakeImpl Lang> { abstract Location getLocation(); /** Gets the corresponding `Node`, if any. */ - Node getNode() { none() } + NodeEx getNodeEx() { none() } + + /** Gets the summary context. */ + ParamNodeOption getSummaryCtx() { none() } + + /** Gets the access path. */ + Ap getAp() { none() } + + /** Gets the corresponding `Node`, if any. */ + final Node getNode() { result = this.getNodeEx().asNode() } predicate isSource() { none() } @@ -2690,7 +2700,11 @@ module MakeImpl Lang> { override Location getLocation() { result = node.getLocation() } - override Node getNode() { result = node.asNode() } + override NodeEx getNodeEx() { result = node } + + override ParamNodeOption getSummaryCtx() { result = summaryCtx } + + override Ap getAp() { result = ap } override predicate isSource() { sourceNode(node, state) and @@ -2728,8 +2742,9 @@ module MakeImpl Lang> { ParamNodeOption summaryCtx, TypOption argT, ApOption argAp, Typ t, Ap ap, boolean allowsFlowThrough ) { - exists(ApApprox apa, boolean allowsFlowThrough0 | - FwdFlowIn::fwdFlowIn(_, arg, _, p, state, outercc, innercc, + exists(DataFlowCall call, ApApprox apa, boolean allowsFlowThrough0 | + callEdgeArgParam(call, _, arg, p, _, ap) and + FwdFlowIn::fwdFlowIn(call, arg, _, p, state, outercc, innercc, summaryCtx, argT, argAp, t, ap, apa, _, allowsFlowThrough0) and if PrevStage::parameterMayFlowThrough(p, apa) then allowsFlowThrough = allowsFlowThrough0 @@ -2744,6 +2759,10 @@ module MakeImpl Lang> { RetNodeEx ret, ParamNodeEx innerSummaryCtx, Typ innerArgT, Ap innerArgAp, ApApprox innerArgApa ) { + callEdgeReturn(call, _, ret, _, _, _, ap) and + callMayFlowThroughRev(call) and + returnMayFlowThrough(ret, _, _, _) and + matchesCall(ccc, call) and fwdFlowThrough0(call, arg, cc, state, ccc, summaryCtx, argT, argAp, t, ap, apa, ret, innerSummaryCtx, innerArgT, innerArgAp, innerArgApa) } @@ -2797,6 +2816,7 @@ module MakeImpl Lang> { DataFlowCall call, CcCall ccc, RetNodeEx ret, boolean allowsFieldFlow, ApApprox innerArgApa, ApApprox apa | + callEdgeReturn(call, _, ret, _, node, allowsFieldFlow, ap) and fwdFlowThroughStep1(pn1, pn2, pn3, call, cc, state, ccc, summaryCtx, argT, argAp, t, ap, apa, ret, innerArgApa) and flowThroughOutOfCall(call, ccc, ret, node, allowsFieldFlow, innerArgApa, apa) and @@ -2818,24 +2838,35 @@ module MakeImpl Lang> { localStep(mid, state0, node, state, false, t, localCc, label) and ap instanceof ApNil ) - or - // store - exists(NodeEx mid, Content c, Typ t0, Ap ap0 | + } + + private predicate storeStep( + StagePathNode pn1, Content c, NodeEx node, FlowState state, Cc cc, + ParamNodeOption summaryCtx, TypOption argT, ApOption argAp, Typ t, Ap ap, string label + ) { + exists(NodeEx mid, Typ t0, Ap ap0 | pn1 = TStagePathNodeMid(mid, state, cc, summaryCtx, argT, argAp, t0, ap0) and fwdFlowStore(mid, t0, ap0, c, t, node, state, cc, summaryCtx, argT, argAp) and + storeStepCand(mid, ap0, c, node, _, + any(DataFlowType containerType | t = getTyp(containerType))) and ap = apCons(c, t0, ap0) and label = "" ) - or - // read + } + + private predicate readStep( + StagePathNode pn1, Content c, NodeEx node, FlowState state, Cc cc, + ParamNodeOption summaryCtx, TypOption argT, ApOption argAp, Typ t, Ap ap, string label + ) { exists(NodeEx mid, Typ t0, Ap ap0 | pn1 = TStagePathNodeMid(mid, state, cc, summaryCtx, argT, argAp, t0, ap0) and - fwdFlowRead(t0, ap0, t, ap, _, mid, node, state, cc, summaryCtx, argT, argAp) and + fwdFlowRead(t0, ap0, t, ap, c, mid, node, state, cc, summaryCtx, argT, argAp) and + readStepCand(mid, c, node) and label = "" ) } - private predicate localStep(StagePathNode pn1, StagePathNode pn2, string label) { + predicate localStep(StagePathNode pn1, StagePathNode pn2, string label) { exists( NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, TypOption argT, ApOption argAp, Typ t0, Ap ap @@ -2843,6 +2874,34 @@ module MakeImpl Lang> { localStep(pn1, node, state, cc, summaryCtx, argT, argAp, t0, ap, label) and pn2 = typeStrengthenToStagePathNode(node, state, cc, summaryCtx, argT, argAp, t0, ap) ) + } + + predicate storeStep(StagePathNode pn1, Content c, StagePathNode pn2, string label) { + exists( + NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, TypOption argT, + ApOption argAp, Typ t0, Ap ap + | + storeStep(pn1, c, node, state, cc, summaryCtx, argT, argAp, t0, ap, label) and + pn2 = typeStrengthenToStagePathNode(node, state, cc, summaryCtx, argT, argAp, t0, ap) + ) + } + + predicate readStep(StagePathNode pn1, Content c, StagePathNode pn2, string label) { + exists( + NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, TypOption argT, + ApOption argAp, Typ t0, Ap ap + | + readStep(pn1, c, node, state, cc, summaryCtx, argT, argAp, t0, ap, label) and + pn2 = typeStrengthenToStagePathNode(node, state, cc, summaryCtx, argT, argAp, t0, ap) + ) + } + + private predicate localScopeStep(StagePathNode pn1, StagePathNode pn2, string label) { + localStep(pn1, pn2, label) + or + storeStep(pn1, _, pn2, label) + or + readStep(pn1, _, pn2, label) or summaryStep(pn1, pn2, label) } @@ -2854,7 +2913,7 @@ module MakeImpl Lang> { or exists(StagePathNode mid, string l1, string l2 | summaryLabel(pn1, mid, l1) and - localStep(mid, pn2, l2) and + localScopeStep(mid, pn2, l2) and summaryLabel = mergeLabels(l1, l2) ) } @@ -2917,16 +2976,20 @@ module MakeImpl Lang> { ) or // flow out of a callable - exists(RetNodeEx ret, CcNoCall innercc, boolean allowsFieldFlow, ApApprox apa | + exists( + DataFlowCall call, RetNodeEx ret, CcNoCall innercc, boolean allowsFieldFlow, + ApApprox apa + | pn1 = TStagePathNodeMid(ret, state, innercc, summaryCtx, argT, argAp, t, ap) and fwdFlowIntoRet(ret, state, innercc, summaryCtx, argT, argAp, t, ap, apa) and fwdFlowOutValidEdge(_, ret, innercc, _, node, cc, apa, allowsFieldFlow) and + callEdgeReturn(call, _, ret, _, node, allowsFieldFlow, ap) and label = "" and if allowsFieldFlow = false then ap instanceof ApNil else any() ) } - private predicate nonLocalStep(StagePathNode pn1, StagePathNode pn2, string label) { + predicate nonLocalStep(StagePathNode pn1, StagePathNode pn2, string label) { exists( NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, TypOption argT, ApOption argAp, Typ t0, Ap ap @@ -2951,7 +3014,7 @@ module MakeImpl Lang> { query predicate edges(StagePathNode pn1, StagePathNode pn2, string key, string val) { key = "provenance" and ( - localStep(pn1, pn2, val) + localScopeStep(pn1, pn2, val) or nonLocalStep(pn1, pn2, val) or @@ -3417,73 +3480,49 @@ module MakeImpl Lang> { predicate enableStoreReadMatching() { any() } - private class NodeExAlias = NodeEx; + final private class NodeExAlias = NodeEx; + + final private class ArgNodeExAlias = ArgNodeEx; + + final private class ParamNodeExAlias = ParamNodeEx; private module StoreReadMatchingInput implements StoreReadMatchingInputSig { class NodeEx = NodeExAlias; - predicate nodeRange(NodeEx node, boolean fromArg) { - exists(PrevStage::Ap ap | - PrevStage::revFlowAp(node, ap) and - ( - ap = true - or - PrevStage::storeStepCand(node, ap, _, _, _, _) - or - PrevStage::readStepCand(_, _, node) - ) - | - exists(PrevStage::Cc cc | PrevStage::fwdFlow(node, _, cc, _, _, _, _, ap, _) | - PrevStage::instanceofCcCall(cc) and - fromArg = true - or - PrevStage::instanceofCcNoCall(cc) and - fromArg = false - ) - ) - } + class ArgNodeEx = ArgNodeExAlias; - predicate localValueStep(NodeEx node1, NodeEx node2) { - exists(FlowState state, PrevStage::ApOption returnAp | - PrevStage::revFlow(node1, pragma[only_bind_into](state), _, - pragma[only_bind_into](returnAp), true) and - PrevStage::revFlow(node2, pragma[only_bind_into](state), _, - pragma[only_bind_into](returnAp), true) and - Stage2Param::localStep(node1, state, node2, state, true, _, _, _) - ) - } + class ParamNodeEx = ParamNodeExAlias; - predicate jumpValueStep = jumpStepEx/2; + class PathNode = PrevStage::Graph::StagePathNode; - pragma[nomagic] - private predicate flowThroughOutOfCall(RetNodeEx ret, NodeEx out) { - exists(DataFlowCall call, CcCall ccc, ReturnKindExt kind | - PrevStage::callEdgeReturn(call, _, ret, kind, out, true, true) and - PrevStage::callMayFlowThroughRev(call) and - PrevStage::returnMayFlowThrough(ret, _, true, kind) and - matchesCall(ccc, call) - ) + predicate localStep(PathNode node1, PathNode node2) { + PrevStage::Graph::localStep(node1, node2, _) } - predicate callEdgeArgParam(NodeEx arg, NodeEx param) { - PrevStage::callEdgeArgParam(_, _, arg, param, true, true) + predicate nonLocalStep(PathNode node1, PathNode node2) { + PrevStage::Graph::nonLocalStep(node1, node2, _) } - predicate callEdgeReturn(NodeEx ret, NodeEx out, boolean mayFlowThrough) { - PrevStage::callEdgeReturn(_, _, ret, _, out, true, true) and - if flowThroughOutOfCall(ret, out) then mayFlowThrough = true else mayFlowThrough = false - } + predicate subpaths = PrevStage::Graph::subpaths/4; - predicate readContentStep = PrevStage::readStepCand/3; + predicate readContentStep(PathNode node1, Content c, PathNode node2) { + PrevStage::Graph::readStep(node1, c, node2, _) + } - predicate storeContentStep(NodeEx node1, Content c, NodeEx node2) { - PrevStage::storeStepCand(node1, _, c, node2, _, _) + predicate storeContentStep(PathNode node1, Content c, PathNode node2) { + PrevStage::Graph::storeStep(node1, c, node2, _) } predicate accessPathConfigLimit = Config::accessPathLimit/0; } - predicate storeMayReachRead = StoreReadMatching::storeMayReachRead/3; + predicate storeMayReachRead(NodeEx storeSource, Content c, NodeEx readTarget) { + exists(StoreReadMatchingInput::PathNode pn1, StoreReadMatchingInput::PathNode pn2 | + StoreReadMatching::storeMayReachRead(pn1, c, pn2) and + storeSource = pn1.getNodeEx() and + readTarget = pn2.getNodeEx() + ) + } } private module Stage3 = MkStage::Stage; diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImplCommon.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImplCommon.qll index 8e64530799321..5a0b554ee1ba7 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImplCommon.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImplCommon.qll @@ -2355,22 +2355,42 @@ module MakeImplCommon Lang> { /** Provides the input to `StoreReadMatching`. */ signature module StoreReadMatchingInputSig { class NodeEx { + Node asNode(); + string toString(); + + Location getLocation(); + } + + class ArgNodeEx extends NodeEx { + DataFlowCall getCall(); } - predicate nodeRange(NodeEx node, boolean fromArg); + class ParamNodeEx extends NodeEx; + + class PathNode { + ParamNodeOption getSummaryCtx(); + + NodeEx getNodeEx(); - predicate localValueStep(NodeEx node1, NodeEx node2); + predicate isSource(); + + predicate isSink(); + + string toString(); + + Location getLocation(); + } - predicate jumpValueStep(NodeEx node1, NodeEx node2); + predicate localStep(PathNode node1, PathNode node2); - predicate callEdgeArgParam(NodeEx arg, NodeEx param); + predicate nonLocalStep(PathNode node1, PathNode node2); - predicate callEdgeReturn(NodeEx ret, NodeEx out, boolean mayFlowThrough); + predicate subpaths(PathNode arg, PathNode par, PathNode ret, PathNode out); - predicate readContentStep(NodeEx node1, Content c, NodeEx node2); + predicate readContentStep(PathNode node1, Content c, PathNode node2); - predicate storeContentStep(NodeEx node1, Content c, NodeEx node2); + predicate storeContentStep(PathNode node1, Content c, PathNode node2); int accessPathConfigLimit(); } @@ -2379,8 +2399,8 @@ module MakeImplCommon Lang> { * Provides logic for computing compatible and (likely) matching store-read pairs. * * In order to determine whether a store can be matched with a compatible read, we - * check whether the target of a store may reach the source of a read, using over- - * approximated data flow (no call contexts). + * check whether the target of a store may reach the source of a read, using a data + * flow graph as input. * * The implementation is based on `doublyBoundedFastTC`, and in order to avoid poor * performance through recursion, we unroll the recursion manually 4 times, in order to @@ -2397,26 +2417,133 @@ module MakeImplCommon Lang> { private import codeql.util.Boolean private import Input + private predicate pathStep(PathNode node1, PathNode node2) { + localStep(node1, node2) + or + nonLocalStep(node1, node2) + or + subpaths(node1, _, _, node2) + or + storeContentStep(node1, _, node2) + or + readContentStep(node1, _, node2) + } + + private predicate pathStepExt(PathNode node1, PathNode node2) { + pathStep(node1, node2) + or + subpaths(_, _, node1, node2) + } + + private predicate reachesSink(PathNode n) { + n.isSink() + or + exists(PathNode succ | + reachesSink(succ) and + pathStepExt(n, succ) + ) + } + + private predicate sourceReaches(PathNode n) { + reachesSink(n) and + ( + n.isSource() + or + exists(PathNode pred | + sourceReaches(pred) and + pathStepExt(pred, n) + ) + ) + } + + /** + * Holds if `arg` may flow into `param` via `call`, and `param` may flow back + * out to `call`. + */ + private predicate pathFlowInThroughStep( + DataFlowCall call, PathNode arg, PathNode param, ParamNodeOption summaryCtx + ) { + exists(ParamNodeEx p | + subpaths(arg, param, _, _) and + param.getNodeEx() = p and + param.getSummaryCtx() = summaryCtx and + summaryCtx = TParamNodeSome(p.asNode()) and + call = arg.getNodeEx().(ArgNodeEx).getCall() + ) + } + + pragma[nomagic] + private predicate localScopeStep(PathNode pn1, PathNode pn2, ParamNodeOption summaryCtx) { + ( + localStep(pn1, pn2) or + subpaths(pn1, _, _, pn2) or + storeContentStep(pn1, _, pn2) or + readContentStep(pn1, _, pn2) + ) and + pn2.getSummaryCtx() = summaryCtx + } + + /** + * Holds if `call` is a relevant flow-through call context for `n`, where + * `p` reaches `n` through local flow, and `p` is the parameter of a target + * of `call`. + */ + pragma[nomagic] + private predicate relevantCallContext(PathNode n, DataFlowCall call, ParamNodeOption summaryCtx) { + pathFlowInThroughStep(call, _, n, summaryCtx) + or + exists(PathNode mid | + relevantCallContext(mid, call, summaryCtx) and + localScopeStep(mid, n, summaryCtx) + ) + } + + private predicate reachesSinkDirect(PathNode n) { + n.isSink() + or + exists(PathNode succ | + pathStep(n, succ) and + reachesSinkDirect(succ) + ) + } + private signature module StoreReachesReadInputSig { int iteration(); predicate storeMayReachReadDelta( - NodeEx storeSource, Content c, NodeEx readTarget, boolean fromArg1, boolean fromArg2 + PathNode storeSource, Content c, PathNode readTarget, DataFlowCallOption callCtx1, + DataFlowCallOption callCtx2 ); predicate storeMayReachReadPrev( - NodeEx storeSource, Content c, NodeEx readTarget, boolean fromArg1, boolean fromArg2 + PathNode storeSource, Content c, PathNode readTarget, DataFlowCallOption callCtx1, + DataFlowCallOption callCtx2 ); } private newtype TNodeOrContent = - TNodeOrContentNode(NodeEx n, Boolean usesPrevDelta, boolean fromArg) { nodeRange(n, fromArg) } or + TNodeOrContentNode(PathNode n, DataFlowCallOption callCtx, Boolean usesPrevDelta) { + sourceReaches(n) and + ( + exists(DataFlowCall call | + relevantCallContext(n, call, _) and + callCtx = TDataFlowCallSome(call) and + n.getSummaryCtx() = TParamNodeSome(_) + ) + or + ( + reachesSinkDirect(n) or + n.getSummaryCtx() = TParamNodeNone() + ) and + callCtx = TDataFlowCallNone() + ) + } or TNodeOrContentStoreContent(Content c) { storeContentStep(_, c, _) } or TNodeOrContentReadContent(Content c) { readContentStep(_, c, _) } private class NodeOrContent extends TNodeOrContent { - NodeEx asNodeEx(boolean usesPrevDelta, boolean fromArg) { - this = TNodeOrContentNode(result, usesPrevDelta, fromArg) + PathNode asPathNode(DataFlowCallOption callCtx, boolean usesPrevDelta) { + this = TNodeOrContentNode(result, callCtx, usesPrevDelta) } Content asStoreContent() { this = TNodeOrContentStoreContent(result) } @@ -2428,30 +2555,52 @@ module MakeImplCommon Lang> { or result = this.asReadContent().toString() or - result = this.asNodeEx(_, _).toString() + result = this.asPathNode(_, _).toString() } } pragma[nomagic] - private predicate stepNodeCommon( - NodeOrContent node1, NodeEx n2, boolean usesPrevDelta2, Boolean fromArg2 + private predicate pureStepNode( + NodeOrContent node1, PathNode n2, DataFlowCallOption callCtx2, boolean usesPrevDelta2 ) { - exists(NodeEx n1, boolean fromArg1 | n1 = node1.asNodeEx(usesPrevDelta2, fromArg1) | - localValueStep(n1, n2) and - fromArg1 = fromArg2 - or - jumpValueStep(n1, n2) and - fromArg2 = false + exists(PathNode n1, DataFlowCallOption callCtx1 | + n1 = node1.asPathNode(callCtx1, usesPrevDelta2) and + n2 = any(NodeOrContent n).asPathNode(_, _) + | + // local step + localStep(n1, n2) and + callCtx2 = callCtx1 or - callEdgeArgParam(n1, n2) and - fromArg2 = true + // flow into a callable with flow-through + exists(DataFlowCall call | + pathFlowInThroughStep(call, n1, n2, _) and + callCtx2 = TDataFlowCallSome(call) + ) or - exists(boolean mayFlowThrough | - callEdgeReturn(n1, n2, mayFlowThrough) and - nodeRange(n2, fromArg2) - | - fromArg1 = false or mayFlowThrough = true + // flow through a callable + exists(DataFlowCall call, PathNode arg, PathNode param | + pathFlowInThroughStep(call, arg, param, _) and + subpaths(arg, param, n1, n2) and + callCtx1 = TDataFlowCallSome(call) and + n2 = any(NodeOrContent n).asPathNode(callCtx2, usesPrevDelta2) ) + or + // non-local step that does not involve flow-through + nonLocalStep(n1, n2) and + not pathFlowInThroughStep(_, n1, n2, _) and + callCtx2 = TDataFlowCallNone() + ) + } + + /** + * Holds if the is a data flow step from `node1` to `node2`, which does + * not store or read content. + */ + pragma[nomagic] + private predicate pureStep(NodeOrContent node1, NodeOrContent node2) { + exists(PathNode n2, DataFlowCallOption callCtx2, boolean usesPrevDelta2 | + n2 = node2.asPathNode(callCtx2, usesPrevDelta2) and + pureStepNode(node1, n2, callCtx2, usesPrevDelta2) ) } @@ -2468,43 +2617,41 @@ module MakeImplCommon Lang> { } pragma[nomagic] - private predicate stepNode( - NodeOrContent node1, NodeEx n2, boolean usesPrevDelta2, Boolean fromArg2 + private predicate prevStepNode( + NodeOrContent node1, PathNode n2, DataFlowCallOption callCtx2, boolean usesPrevDelta2 ) { enabled() and - ( - stepNodeCommon(node1, n2, usesPrevDelta2, fromArg2) + exists(PathNode n1, DataFlowCallOption callCtx1, boolean usesPrevDelta1 | + n1 = node1.asPathNode(callCtx1, usesPrevDelta1) + | + Prev::storeMayReachReadDelta(n1, _, n2, callCtx1, callCtx2) and + usesPrevDelta2 = true or - exists(NodeEx n1, boolean usesPrevDelta1, boolean fromArg1 | - n1 = node1.asNodeEx(usesPrevDelta1, fromArg1) - | - Prev::storeMayReachReadDelta(n1, _, n2, fromArg1, fromArg2) and - usesPrevDelta2 = true - or - Prev::storeMayReachReadPrev(n1, _, n2, fromArg1, fromArg2) and - usesPrevDelta1 = usesPrevDelta2 - ) + Prev::storeMayReachReadPrev(n1, _, n2, callCtx1, callCtx2) and + usesPrevDelta1 = usesPrevDelta2 ) } pragma[nomagic] private predicate step(NodeOrContent node1, NodeOrContent node2) { - exists(NodeEx n2, boolean usesPrevDelta2, boolean fromArg2 | - n2 = node2.asNodeEx(usesPrevDelta2, fromArg2) and - stepNode(node1, n2, usesPrevDelta2, fromArg2) - ) - or enabled() and ( - exists(NodeEx n2, Content c, boolean usesPrevDelta2 | - n2 = node2.asNodeEx(usesPrevDelta2, _) and + pureStep(node1, node2) + or + exists(PathNode n2, DataFlowCallOption callCtx2, boolean usesPrevDelta2 | + n2 = node2.asPathNode(callCtx2, usesPrevDelta2) and + prevStepNode(node1, n2, callCtx2, usesPrevDelta2) + ) + or + exists(PathNode n2, Content c, boolean usesPrevDelta2 | + n2 = node2.asPathNode(_, usesPrevDelta2) and c = node1.asStoreContent() and storeContentStep(_, c, n2) and usesPrevDelta2 = false ) or - exists(NodeEx n1, Content c, boolean usesPrevDelta1 | - n1 = node1.asNodeEx(usesPrevDelta1, _) and + exists(PathNode n1, Content c, boolean usesPrevDelta1 | + n1 = node1.asPathNode(_, usesPrevDelta1) and c = node2.asReadContent() and readContentStep(n1, c, _) and usesPrevDelta(usesPrevDelta1) @@ -2543,7 +2690,7 @@ module MakeImplCommon Lang> { private predicate isStoreTarget0(NodeOrContent node, Content c) { exists(boolean usesPrevDelta | contentIsReadAndStored(c) and - storeContentStep(_, c, node.asNodeEx(usesPrevDelta, _)) and + storeContentStep(_, c, node.asPathNode(_, usesPrevDelta)) and usesPrevDelta = false ) } @@ -2554,7 +2701,7 @@ module MakeImplCommon Lang> { private predicate isReadSource0(NodeOrContent node, Content c) { exists(boolean usesPrevDelta | contentIsReadAndStored(c) and - readContentStep(node.asNodeEx(usesPrevDelta, _), c, _) and + readContentStep(node.asPathNode(_, usesPrevDelta), c, _) and usesPrevDelta(usesPrevDelta) ) } @@ -2602,45 +2749,47 @@ module MakeImplCommon Lang> { pragma[nomagic] private predicate storeMayReachReadDeltaJoinLeft( - NodeEx node1, Content c, NodeOrContent node2, boolean fromArg + PathNode node1, Content c, NodeOrContent node2, DataFlowCallOption callCtx2 ) { exists(boolean usesPrevDelta | storeMayReachARead(pragma[only_bind_into](node2), pragma[only_bind_into](c)) and - storeContentStep(node1, c, node2.asNodeEx(usesPrevDelta, fromArg)) and + storeContentStep(node1, c, node2.asPathNode(callCtx2, usesPrevDelta)) and usesPrevDelta = false ) } pragma[nomagic] private predicate storeMayReachReadDeltaJoinRight( - NodeOrContent node1, Content c, NodeEx node2, boolean fromArg + NodeOrContent node1, DataFlowCallOption callCtx1, Content c, PathNode node2 ) { exists(boolean usesPrevDelta | aStoreMayReachRead(pragma[only_bind_into](node1), pragma[only_bind_into](c)) and - readContentStep(node1.asNodeEx(usesPrevDelta, fromArg), c, node2) and + readContentStep(node1.asPathNode(callCtx1, usesPrevDelta), c, node2) and usesPrevDelta(usesPrevDelta) ) } pragma[nomagic] predicate storeMayReachReadDelta( - NodeEx storeSource, Content c, NodeEx readTarget, boolean fromArg1, boolean fromArg2 + PathNode storeSource, Content c, PathNode readTarget, DataFlowCallOption callCtx1, + DataFlowCallOption callCtx2 ) { exists(NodeOrContent storeTarget, NodeOrContent readSource | storeMayReachReadTc(storeTarget, readSource) and - storeMayReachReadDeltaJoinLeft(storeSource, c, storeTarget, fromArg1) and - storeMayReachReadDeltaJoinRight(readSource, c, readTarget, fromArg2) + storeMayReachReadDeltaJoinLeft(storeSource, c, storeTarget, callCtx1) and + storeMayReachReadDeltaJoinRight(readSource, callCtx2, c, readTarget) ) and - not Prev::storeMayReachReadPrev(storeSource, c, readTarget, fromArg1, fromArg2) + not Prev::storeMayReachReadPrev(storeSource, c, readTarget, callCtx1, callCtx2) } pragma[nomagic] predicate storeMayReachReadPrev( - NodeEx storeSource, Content c, NodeEx readTarget, boolean fromArg1, boolean fromArg2 + PathNode storeSource, Content c, PathNode readTarget, DataFlowCallOption callCtx1, + DataFlowCallOption callCtx2 ) { - Prev::storeMayReachReadPrev(storeSource, c, readTarget, fromArg1, fromArg2) + Prev::storeMayReachReadPrev(storeSource, c, readTarget, callCtx1, callCtx2) or - Prev::storeMayReachReadDelta(storeSource, c, readTarget, fromArg1, fromArg2) + Prev::storeMayReachReadDelta(storeSource, c, readTarget, callCtx1, callCtx2) } } @@ -2648,13 +2797,15 @@ module MakeImplCommon Lang> { int iteration() { result = 0 } predicate storeMayReachReadDelta( - NodeEx node1, Content c, NodeEx node2, boolean fromArg1, boolean fromArg2 + PathNode node1, Content c, PathNode node2, DataFlowCallOption callCtx1, + DataFlowCallOption callCtx2 ) { none() } predicate storeMayReachReadPrev( - NodeEx node1, Content c, NodeEx node2, boolean fromArg1, boolean fromArg2 + PathNode node1, Content c, PathNode node2, DataFlowCallOption callCtx1, + DataFlowCallOption callCtx2 ) { none() } @@ -2666,19 +2817,19 @@ module MakeImplCommon Lang> { import M predicate storeMayReachReadDelta( - NodeEx storeSource, Content c, NodeEx readTarget, boolean fromArg1, boolean fromArg2 + PathNode storeSource, Content c, PathNode readTarget, DataFlowCallOption callCtx1, + DataFlowCallOption callCtx2 ) { - M::storeMayReachReadDelta(storeSource, c, readTarget, fromArg1, fromArg2) + M::storeMayReachReadDelta(storeSource, c, readTarget, callCtx1, callCtx2) or // special case only needed for the first iteration: a store immediately followed by a read - exists(NodeEx storeTargetReadSource | + exists(PathNode storeTargetReadSource | StoreReachesRead1::contentIsReadAndStored(c) and storeContentStep(storeSource, c, storeTargetReadSource) and - readContentStep(storeTargetReadSource, c, readTarget) - ) and - nodeRange(storeSource, fromArg1) and - nodeRange(readTarget, fromArg2) and - fromArg1 = fromArg2 + readContentStep(storeTargetReadSource, c, readTarget) and + storeTargetReadSource = any(NodeOrContent n).asPathNode(callCtx1, _) and + callCtx2 = callCtx1 + ) } } @@ -2690,7 +2841,7 @@ module MakeImplCommon Lang> { private module StoreReachesRead5 = StoreReachesRead; - predicate storeMayReachRead(NodeEx storeSource, Content c, NodeEx readTarget) { + predicate storeMayReachRead(PathNode storeSource, Content c, PathNode readTarget) { StoreReachesRead5::storeMayReachReadDelta(storeSource, c, readTarget, _, _) or StoreReachesRead5::storeMayReachReadPrev(storeSource, c, readTarget, _, _)