From 2f2e049be71372de27fe2552710c2903538f34cc Mon Sep 17 00:00:00 2001 From: Tom Hvitved Date: Fri, 12 Jul 2024 14:02:54 +0200 Subject: [PATCH] Data flow: Compute local big step relation per stage --- .../codeql/dataflow/internal/DataFlowImpl.qll | 455 +++++++++--------- 1 file changed, 229 insertions(+), 226 deletions(-) diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll index 6eb1efc2b3da2..076554ab64169 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll @@ -1074,18 +1074,6 @@ module MakeImpl Lang> { if label1 = "" then result = label2 else result = label1 } - pragma[noinline] - private predicate localFlowStepNodeCand1(NodeEx node1, NodeEx node2, string model) { - Stage1::revFlow(node2) and - localFlowStepEx(node1, node2, model) - } - - pragma[noinline] - private predicate additionalLocalFlowStepNodeCand1(NodeEx node1, NodeEx node2, string model) { - Stage1::revFlow(node2) and - additionalLocalFlowStep(node1, node2, model) - } - pragma[nomagic] private predicate viableReturnPosOutNodeCand1(DataFlowCall call, ReturnPosition pos, NodeEx out) { Stage1::revFlow(out) and @@ -1406,7 +1394,7 @@ module MakeImpl Lang> { bindingset[node2, state2] predicate localStep( NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue, - Typ t, LocalCc lcc + Typ t, LocalCc lcc, string label ); bindingset[node, state, t0, ap] @@ -1524,10 +1512,10 @@ module MakeImpl Lang> { fwdFlow(mid, state0, cc, summaryCtx, argT, argAp, t0, ap, apa) and localCc = getLocalCc(cc) | - localStep(mid, state0, node, state, true, _, localCc) and + localStep(mid, state0, node, state, true, _, localCc, _) and t = t0 or - localStep(mid, state0, node, state, false, t, localCc) and + localStep(mid, state0, node, state, false, t, localCc, _) and ap instanceof ApNil ) or @@ -2174,12 +2162,12 @@ module MakeImpl Lang> { ap instanceof ApNil or exists(NodeEx mid, FlowState state0 | - localStep(node, state, mid, state0, true, _, _) and + localStep(node, state, mid, state0, true, _, _, _) and revFlow(mid, state0, returnCtx, returnAp, ap) ) or exists(NodeEx mid, FlowState state0 | - localStep(node, pragma[only_bind_into](state), mid, state0, false, _, _) and + localStep(node, pragma[only_bind_into](state), mid, state0, false, _, _, _) and revFlow(mid, state0, returnCtx, returnAp, ap) and ap instanceof ApNil ) @@ -2519,6 +2507,199 @@ module MakeImpl Lang> { callEdgeReturn(call, c, _, _, _, _, _) } + /** Provides a big-step relation for local flow steps. */ + additional module LocalFlowBigStep { + bindingset[node1, state1] + private predicate localStep( + NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue, + string label + ) { + localStep(node1, state1, node2, state2, preservesValue, _, _, label) + } + + private predicate flowIntoCall(ArgNodeEx node1, ParamNodeEx node2) { + callEdgeArgParam(_, _, node1, node2, _, _) + } + + private predicate flowOutOfCall(RetNodeEx node1, NodeEx node2) { + callEdgeReturn(_, _, node1, _, node2, _, _) + } + + final private class NodeExFinal = NodeEx; + + /** + * A node where some checking is required, and hence the big-step relation + * is not allowed to step over. + */ + private class FlowCheckNode extends NodeExFinal { + FlowCheckNode() { + revFlow(this, _, _) and + ( + castNode(this.asNode()) or + clearsContentCached(this.asNode(), _) or + expectsContentCached(this.asNode(), _) or + neverSkipInPathGraph(this.asNode()) or + Config::neverSkip(this.asNode()) + ) + } + } + + private predicate additionalLocalStateStep( + NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, string label + ) { + exists(ApNil nil | + revFlow(node1, state1, nil) and + revFlow(node2, state2, nil) and + localStep(node1, state1, node2, state2, false, label) and + state1 != state2 + ) + } + + /** + * Holds if `node` can be the first node in a maximal subsequence of local + * flow steps in a dataflow path. + */ + private predicate localFlowEntry(NodeEx node, FlowState state, Ap ap) { + revFlow(node, state, ap) and + ( + sourceNode(node, state) + or + jumpStepEx(_, node) + or + additionalJumpStep(_, node, _) + or + additionalJumpStateStep(_, _, node, state) + or + node instanceof ParamNodeEx + or + node.asNode() instanceof OutNodeExt + or + storeEx(_, _, node, _, _) + or + readSetEx(_, _, node) + or + node instanceof FlowCheckNode + or + exists(FlowState s | + additionalLocalStateStep(_, s, node, state, _) and + s != state + ) + ) + } + + /** + * Holds if `node` can be the last node in a maximal subsequence of local + * flow steps in a dataflow path. + */ + private predicate localFlowExit(NodeEx node, FlowState state, Ap ap) { + revFlow(node, pragma[only_bind_into](state), pragma[only_bind_into](ap)) and + ( + exists(NodeEx next, Ap apNext | revFlow(next, pragma[only_bind_into](state), apNext) | + jumpStepEx(node, next) and + apNext = ap + or + additionalJumpStep(node, next, _) and + apNext = ap and + ap instanceof ApNil + or + flowIntoCall(node, next) and + apNext = ap + or + flowOutOfCall(node, next) and + apNext = ap + or + storeEx(node, _, next, _, _) + or + readSetEx(node, _, next) + ) + or + exists(NodeEx next, FlowState s | + revFlow(next, s, pragma[only_bind_into](ap)) and ap instanceof ApNil + | + additionalJumpStateStep(node, state, next, s) + or + additionalLocalStateStep(node, state, next, s) and + s != state + ) + or + node instanceof FlowCheckNode + or + sinkNode(node, state) and + ap instanceof ApNil + ) + } + + /** + * Holds if the local path from `node1` to `node2` is a prefix of a maximal + * subsequence of local flow steps in a dataflow path. + * + * This is the transitive closure of `[additional]localFlowStep` beginning + * at `localFlowEntry`. + */ + pragma[nomagic] + private predicate localFlowStepPlus( + NodeEx node1, FlowState state, NodeEx node2, boolean preservesValue, DataFlowType t, + LocalCallContext cc, string label + ) { + not isUnreachableInCall1(node2, cc) and + not inBarrier(node2, state) and + not outBarrier(node1, state) and + exists(NodeEx node0, boolean preservesValue0, string label0, Ap ap | + localStep(node0, state, node2, state, preservesValue0, label0) and + revFlow(node2, pragma[only_bind_into](state), pragma[only_bind_into](ap)) and + not outBarrier(node0, state) and + (preservesValue = true or ap instanceof ApNil) + | + node1 = node0 and + localFlowEntry(node1, pragma[only_bind_into](state), pragma[only_bind_into](ap)) and + preservesValue = preservesValue0 and + label = label0 and + ( + if preservesValue = true + then t = node1.getDataFlowType() // irrelevant dummy value + else t = node2.getDataFlowType() + ) and + node1 != node2 and + cc.relevantFor(node1.getEnclosingCallable()) and + not isUnreachableInCall1(node1, cc) + or + exists(boolean preservesValue1, DataFlowType t1, string label1 | + localFlowStepPlus(node1, pragma[only_bind_into](state), node0, preservesValue1, t1, + cc, label1) and + not node0 instanceof FlowCheckNode and + preservesValue = preservesValue0.booleanAnd(preservesValue1) and + label = mergeLabels(label0, label1) and + if preservesValue = true then t = t1 else t = node2.getDataFlowType() + ) + ) + } + + /** + * Holds if `node1` can step to `node2` in one or more local steps and this + * path can occur as a maximal subsequence of local steps in a dataflow path. + */ + pragma[nomagic] + predicate localFlowBigStep( + NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue, + DataFlowType t, LocalCallContext callContext, string label + ) { + exists(Ap ap | + localFlowStepPlus(node1, state1, node2, preservesValue, t, callContext, label) and + localFlowExit(node2, state1, ap) and + state1 = state2 + | + preservesValue = true or ap instanceof ApNil + ) + or + additionalLocalStateStep(node1, state1, node2, state2, label) and + preservesValue = false and + t = node2.getDataFlowType() and + callContext.relevantFor(node1.getEnclosingCallable()) and + not isUnreachableInCall1(node1, callContext) and + not isUnreachableInCall1(node2, callContext) + } + } + /** * INTERNAL: Only for debugging. * @@ -2683,10 +2864,10 @@ module MakeImpl Lang> { pn1 = TStagePathNodeMid(mid, state0, cc, summaryCtx, argT, argAp, t0, ap) and localCc = getLocalCc(cc) | - localStep(mid, state0, node, state, true, _, localCc) and + localStep(mid, state0, node, state, true, _, localCc, _) and t = t0 or - localStep(mid, state0, node, state, false, t, localCc) and + localStep(mid, state0, node, state, false, t, localCc, _) and ap instanceof ApNil ) or @@ -2913,23 +3094,36 @@ module MakeImpl Lang> { import CachedCallContextSensitivity import NoLocalCallContext + pragma[noinline] + private predicate localFlowStepNodeCand1(NodeEx node1, NodeEx node2, string model) { + Stage1::revFlow(node2) and + localFlowStepEx(node1, node2, model) + } + + pragma[nomagic] + private predicate additionalLocalFlowStepNodeCand1(NodeEx node1, NodeEx node2, string model) { + Stage1::revFlow(node2) and + additionalLocalFlowStep(node1, node2, model) + } + bindingset[node1, state1] bindingset[node2, state2] predicate localStep( NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue, - Typ t, LocalCc lcc + Typ t, LocalCc lcc, string label ) { ( preservesValue = true and - localFlowStepNodeCand1(node1, node2, _) and + localFlowStepNodeCand1(node1, node2, label) and state1 = state2 or preservesValue = false and - additionalLocalFlowStepNodeCand1(node1, node2, _) and + additionalLocalFlowStepNodeCand1(node1, node2, label) and state1 = state2 or preservesValue = false and - additionalLocalStateStep(node1, state1, node2, state2) + additionalLocalStateStep(node1, state1, node2, state2) and + label = "Config" ) and exists(t) and exists(lcc) @@ -2966,192 +3160,6 @@ module MakeImpl Lang> { private module Stage2 = MkStage::Stage; - pragma[nomagic] - private predicate flowOutOfCallNodeCand2( - DataFlowCall call, RetNodeEx node1, ReturnKindExt kind, NodeEx node2, boolean allowsFieldFlow - ) { - flowOutOfCallNodeCand1(call, node1, kind, node2, allowsFieldFlow) and - Stage2::revFlow(node2) and - Stage2::revFlow(node1) - } - - pragma[nomagic] - private predicate flowIntoCallNodeCand2( - DataFlowCall call, ArgNodeEx node1, ParamNodeEx node2, boolean allowsFieldFlow - ) { - flowIntoCallNodeCand1(call, node1, node2, allowsFieldFlow) and - Stage2::revFlow(node2) and - Stage2::revFlow(node1) - } - - private module LocalFlowBigStep { - /** - * A node where some checking is required, and hence the big-step relation - * is not allowed to step over. - */ - private class FlowCheckNode extends NodeEx { - FlowCheckNode() { - castNode(this.asNode()) or - clearsContentCached(this.asNode(), _) or - expectsContentCached(this.asNode(), _) or - neverSkipInPathGraph(this.asNode()) or - Config::neverSkip(this.asNode()) - } - } - - /** - * Holds if `node` can be the first node in a maximal subsequence of local - * flow steps in a dataflow path. - */ - private predicate localFlowEntry(NodeEx node, FlowState state) { - Stage2::revFlow(node, state) and - ( - sourceNode(node, state) - or - jumpStepEx(_, node) - or - additionalJumpStep(_, node, _) - or - additionalJumpStateStep(_, _, node, state) - or - node instanceof ParamNodeEx - or - node.asNode() instanceof OutNodeExt - or - Stage2::storeStepCand(_, _, _, node, _, _) - or - Stage2::readStepCand(_, _, node) - or - node instanceof FlowCheckNode - or - exists(FlowState s | - additionalLocalStateStep(_, s, node, state) and - s != state - ) - ) - } - - /** - * Holds if `node` can be the last node in a maximal subsequence of local - * flow steps in a dataflow path. - */ - private predicate localFlowExit(NodeEx node, FlowState state) { - exists(NodeEx next | Stage2::revFlow(next, state) | - jumpStepEx(node, next) or - additionalJumpStep(node, next, _) or - flowIntoCallNodeCand2(_, node, next, _) or - flowOutOfCallNodeCand2(_, node, _, next, _) or - Stage2::storeStepCand(node, _, _, next, _, _) or - Stage2::readStepCand(node, _, next) - ) - or - exists(NodeEx next, FlowState s | Stage2::revFlow(next, s) | - additionalJumpStateStep(node, state, next, s) - or - additionalLocalStateStep(node, state, next, s) and - s != state - ) - or - Stage2::revFlow(node, state) and - node instanceof FlowCheckNode - or - sinkNode(node, state) - } - - pragma[noinline] - private predicate additionalLocalFlowStepNodeCand2( - NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, string label - ) { - additionalLocalFlowStepNodeCand1(node1, node2, label) and - state1 = state2 and - Stage2::revFlow(node1, pragma[only_bind_into](state1), false) and - Stage2::revFlow(node2, pragma[only_bind_into](state2), false) - or - additionalLocalStateStep(node1, state1, node2, state2) and - label = "Config" and - Stage2::revFlow(node1, state1, false) and - Stage2::revFlow(node2, state2, false) - } - - /** - * Holds if the local path from `node1` to `node2` is a prefix of a maximal - * subsequence of local flow steps in a dataflow path. - * - * This is the transitive closure of `[additional]localFlowStep` beginning - * at `localFlowEntry`. - */ - pragma[nomagic] - private predicate localFlowStepPlus( - NodeEx node1, FlowState state, NodeEx node2, boolean preservesValue, DataFlowType t, - LocalCallContext cc, string label - ) { - not isUnreachableInCall1(node2, cc) and - not inBarrier(node2, state) and - not outBarrier(node1, state) and - ( - localFlowEntry(node1, pragma[only_bind_into](state)) and - ( - localFlowStepNodeCand1(node1, node2, label) and - preservesValue = true and - t = node1.getDataFlowType() and // irrelevant dummy value - Stage2::revFlow(node2, pragma[only_bind_into](state)) - or - additionalLocalFlowStepNodeCand2(node1, state, node2, state, label) and - preservesValue = false and - t = node2.getDataFlowType() - ) and - node1 != node2 and - cc.relevantFor(node1.getEnclosingCallable()) and - not isUnreachableInCall1(node1, cc) and - not outBarrier(node1, state) - or - exists(NodeEx mid, string label1, string label2 | - localFlowStepPlus(node1, pragma[only_bind_into](state), mid, preservesValue, t, cc, - label1) and - localFlowStepNodeCand1(mid, node2, label2) and - not outBarrier(mid, state) and - not mid instanceof FlowCheckNode and - Stage2::revFlow(node2, pragma[only_bind_into](state)) and - label = mergeLabels(label1, label2) - ) - or - exists(NodeEx mid, string label1, string label2 | - localFlowStepPlus(node1, state, mid, _, _, cc, label1) and - additionalLocalFlowStepNodeCand2(mid, state, node2, state, label2) and - not outBarrier(mid, state) and - not mid instanceof FlowCheckNode and - preservesValue = false and - t = node2.getDataFlowType() and - label = mergeLabels(label1, label2) - ) - ) - } - - /** - * Holds if `node1` can step to `node2` in one or more local steps and this - * path can occur as a maximal subsequence of local steps in a dataflow path. - */ - pragma[nomagic] - predicate localFlowBigStep( - NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue, - DataFlowType t, LocalCallContext callContext, string label - ) { - localFlowStepPlus(node1, state1, node2, preservesValue, t, callContext, label) and - localFlowExit(node2, state1) and - state1 = state2 - or - additionalLocalFlowStepNodeCand2(node1, state1, node2, state2, label) and - state1 != state2 and - preservesValue = false and - t = node2.getDataFlowType() and - callContext.relevantFor(node1.getEnclosingCallable()) and - not isUnreachableInCall1(node1, callContext) and - not isUnreachableInCall1(node2, callContext) - } - } - - private import LocalFlowBigStep - pragma[nomagic] private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode or exists(node.asParamReturnNode()) @@ -3203,9 +3211,10 @@ module MakeImpl Lang> { predicate localStep( NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue, - Typ t, LocalCc lcc + Typ t, LocalCc lcc, string label ) { - localFlowBigStep(node1, state1, node2, state2, preservesValue, _, _, _) and + PrevStage::LocalFlowBigStep::localFlowBigStep(node1, state1, node2, state2, preservesValue, + _, _, label) and exists(t) and exists(lcc) } @@ -3290,11 +3299,10 @@ module MakeImpl Lang> { pragma[nomagic] predicate localStep( NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue, - Typ t, LocalCc lcc + Typ t, LocalCc lcc, string label ) { - localFlowBigStep(node1, state1, node2, state2, preservesValue, t, _, _) and - PrevStage::revFlow(node1, pragma[only_bind_into](state1), _) and - PrevStage::revFlow(node2, pragma[only_bind_into](state2), _) and + PrevStage::LocalFlowBigStep::localFlowBigStep(node1, state1, node2, state2, preservesValue, + t, _, label) and exists(lcc) } @@ -3590,14 +3598,7 @@ module MakeImpl Lang> { import CallContextSensitivity import LocalCallContext - predicate localStep( - NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue, - Typ t, LocalCc lcc - ) { - localFlowBigStep(node1, state1, node2, state2, preservesValue, t, lcc, _) and - PrevStage::revFlow(node1, pragma[only_bind_into](state1), _) and - PrevStage::revFlow(node2, pragma[only_bind_into](state2), _) - } + predicate localStep = PrevStage::LocalFlowBigStep::localFlowBigStep/8; bindingset[node, state, t0, ap] predicate filter(NodeEx node, FlowState state, Typ t0, Ap ap, Typ t) { @@ -4447,14 +4448,16 @@ module MakeImpl Lang> { ) { exists(NodeEx midnode, FlowState state0, string sl, LocalCallContext localCC | pathNode(mid, midnode, state0, cc, sc, t, ap, sl, localCC) and - localFlowBigStep(midnode, state0, node, state, true, _, localCC, label) and + Stage5::LocalFlowBigStep::localFlowBigStep(midnode, state0, node, state, true, _, localCC, + label) and isStoreStep = false and summaryLabel = mergeLabels(sl, label) ) or exists(NodeEx midnode, FlowState state0, string sl, LocalCallContext localCC | pathNode(mid, midnode, state0, cc, sc, _, ap, sl, localCC) and - localFlowBigStep(midnode, state0, node, state, false, t, localCC, label) and + Stage5::LocalFlowBigStep::localFlowBigStep(midnode, state0, node, state, false, t, localCC, + label) and ap instanceof AccessPathNil and isStoreStep = false and summaryLabel = mergeLabels(sl, label) @@ -4761,7 +4764,7 @@ module MakeImpl Lang> { private PathNodeImpl localStep(PathNodeImpl n) { n.getASuccessorImpl(_) = result and exists(NodeEx n1, NodeEx n2 | n1 = n.getNodeEx() and n2 = result.getNodeEx() | - localFlowBigStep(n1, _, n2, _, _, _, _, _) or + Stage5::LocalFlowBigStep::localFlowBigStep(n1, _, n2, _, _, _, _, _) or storeEx(n1, _, n2, _, _) or readSetEx(n1, _, n2) )