Skip to content

Commit

Permalink
wip
Browse files Browse the repository at this point in the history
  • Loading branch information
hvitved committed Oct 22, 2024
1 parent acd85a3 commit a974c9f
Showing 1 changed file with 27 additions and 25 deletions.
52 changes: 27 additions & 25 deletions shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll
Original file line number Diff line number Diff line change
Expand Up @@ -2606,6 +2606,23 @@ module MakeImpl<LocationSig Location, InputSig<Location> 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.
*
Expand All @@ -2614,25 +2631,6 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
* reachable in this stage.
*/
additional module LocalFlowBigStep<LocalFlowBigStepInputSig Input> {
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, DataFlowType t,
LocalCallContext lcc, string label
Expand Down Expand Up @@ -4414,15 +4412,19 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
private predicate smallStep = Stage3Param::BigStepInput::localStep/8;

private predicate localStepCand(
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue
) {
PrevStage::revFlow(node1, state1, _) and
smallStep(node1, state1, node2, state2, _, _, _, _)
Stage5Param::localStep(node1, state1, _, _, _, _, _, _) and
smallStep(node1, state1, node2, state2, preservesValue, _, _, _)
or
exists(FlowState midState, NodeEx midNode |
localStepCand(node1, state1, midNode, midState) and
localStepCand(node1, state1, midNode, midState, preservesValue) and
smallStep(midNode, midState, node2, state2, _, _, _, _) and
not Stage5Param::localStep(midNode, midState, _, _, _, _, _, _)
not (
Stage5Param::localStep(midNode, midState, _, _, _, _, _, _) and
Stage5Param::localStep(_, _, midNode, midState, _, _, _, _)
) and
not midNode instanceof Stage5::FlowCheckNode
)
}

Expand All @@ -4439,7 +4441,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
DataFlowType t, LocalCallContext lcc, string label
) {
localStepCand(node1, state1, node2, state2) and
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), _)
Expand Down

0 comments on commit a974c9f

Please sign in to comment.