From 02e4731d2cdf1539540b7a27a08e25c7176827fe Mon Sep 17 00:00:00 2001 From: Tom Hvitved Date: Tue, 22 Oct 2024 11:15:12 +0200 Subject: [PATCH] wip2 --- .../codeql/dataflow/internal/DataFlowImpl.qll | 98 ++++++++----------- 1 file changed, 40 insertions(+), 58 deletions(-) diff --git a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll index 0ffc0c0f844c..0250f4d36284 100644 --- a/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll +++ b/shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll @@ -2606,23 +2606,6 @@ module MakeImpl Lang> { ); } - /** - * A node where some checking is required, and hence the big-step relation - * is not allowed to step over. - */ - additional class FlowCheckNode extends NodeEx { - FlowCheckNode() { - revFlow(this, _, _) and - ( - castNode(this.asNode()) or - clearsContentCached(this.asNode(), _) or - expectsContentCached(this.asNode(), _) or - neverSkipInPathGraph(this.asNode()) or - Config::neverSkip(this.asNode()) - ) - } - } - /** * Provides a big-step relation for local flow steps. * @@ -2631,6 +2614,23 @@ module MakeImpl Lang> { * reachable in this stage. */ additional 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() { + 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, DataFlowType t, LocalCallContext lcc, string label @@ -2647,7 +2647,7 @@ module MakeImpl Lang> { * 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) { + predicate localFlowEntry(NodeEx node, FlowState state, Ap ap) { revFlow(node, state, ap) and ( sourceNode(node, state) @@ -2679,7 +2679,7 @@ module MakeImpl Lang> { * 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) { + 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) | @@ -3788,7 +3788,7 @@ module MakeImpl Lang> { import CallContextSensitivity import NoLocalCallContext - additional module BigStepInput implements PrevStage::LocalFlowBigStepInputSig { + private module BigStepInput implements PrevStage::LocalFlowBigStepInputSig { bindingset[node1, state1] bindingset[node2, state2] predicate localStep( @@ -4409,46 +4409,28 @@ module MakeImpl Lang> { import LocalCallContext private module BigStepInput implements PrevStage::LocalFlowBigStepInputSig { - private predicate smallStep = Stage3Param::BigStepInput::localStep/8; - - private predicate localStepCand( - NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue - ) { - Stage5Param::localStep(node1, state1, _, _, _, _, _, _) and - smallStep(node1, state1, node2, state2, preservesValue, _, _, _) - or - exists(FlowState midState, NodeEx midNode | - localStepCand(node1, state1, midNode, midState, preservesValue) and - smallStep(midNode, midState, node2, state2, _, _, _, _) and - not ( - Stage5Param::localStep(midNode, midState, _, _, _, _, _, _) and - Stage5Param::localStep(_, _, midNode, midState, _, _, _, _) - ) and - not midNode instanceof Stage5::FlowCheckNode - ) - } - - /** - * When calculating `localFlowBigStep` based on `Stage5Param::localStep`, which - * is already a big-step relation, we must be careful to avoid quadratic blowup. - * - * This is achieved by restricting `Stage5Param::localStep` to those node pairs - * reacheable via 1 or more `smallStep`s, where any intermediate node is not - * already part of `Stage5Param::localStep`. - */ - pragma[nomagic] - predicate localStep( - NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue, - DataFlowType t, LocalCallContext lcc, string label - ) { - localStepCand(node1, state1, node2, state2, preservesValue) and - Stage5Param::localStep(node1, state1, node2, state2, preservesValue, t, lcc, label) and - PrevStage::revFlow(node1, pragma[only_bind_into](state1), _) and - PrevStage::revFlow(node2, pragma[only_bind_into](state2), _) - } + predicate localStep = Stage5Param::localStep/8; } - predicate localStep = PrevStage::LocalFlowBigStep::localFlowBigStep/8; + pragma[nomagic] + predicate localStep( + NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue, + DataFlowType t, LocalCallContext lcc, string label + ) { + // The following should be equivalent to + // + // ``` + // PrevStage::LocalFlowBigStep::localFlowBigStep + // ``` + // + // but avoids computing the big-step relation based on an existing big-step + // releation, which may have worst-case quadratic complexity. + exists(AccessPathApprox ap | + BigStepInput::localStep(node1, state1, node2, state2, preservesValue, t, lcc, label) and + PrevStage::LocalFlowBigStep::localFlowEntry(node1, state1, ap) and + PrevStage::LocalFlowBigStep::localFlowExit(node2, state2, ap) + ) + } bindingset[node, state, t0, ap] predicate filter(NodeEx node, FlowState state, Typ t0, Ap ap, Typ t) {