Data flow: Prevent quadratic blowup in Stage6Param::localStep
#17739
Conversation
hvitved
force-pushed
the
dataflow/big-step-quadratic
branch
from
6fabf09 to
e54a030
Compare
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
hvitved
force-pushed
the
dataflow/big-step-quadratic
branch
from
e54a030 to
9b37ff4
Compare
hvitved
force-pushed
the
dataflow/big-step-quadratic
branch
5 times, most recently
from
cda67b3 to
380e563
Compare
hvitved
force-pushed
the
dataflow/big-step-quadratic
branch
from
380e563 to
7a2105b
Compare
| ) { | ||
| Stage3Param::localFlowBigStep(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), _) |
There was a problem hiding this comment.
Is the revFlow check that was here lost, or do we preserve it somewhere?
There was a problem hiding this comment.
It's not lost, since it's part of localFlowBigStepTc.
There was a problem hiding this comment.
I'll take your word for it!
| * The big-step releation is based on the `localStep` relation from the | ||
| * input module, restricted to nodes that are forwards and backwards | ||
| * reachable in this stage. | ||
| * The big-step releation is based on the `localStepInput` relation, |
There was a problem hiding this comment.
| * The big-step releation is based on the `localStepInput` relation, | |
| * The big-step relation is based on the `localStepInput` relation, |
| @@ -2769,6 +2765,33 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> { | |||
| exists(Ap ap | | |||
| localFlowStepPlus(node1, state1, node2, preservesValue, t, callContext, label) and | |||
| localFlowExit(node2, state1, ap) and | |||
| state1 = state2 and | |||
| node1 != node2 | |||
There was a problem hiding this comment.
While the addition here might well preserve semantics relative to main, then I don't think it matches what we want and the semantics prior to the introduction of the big-step recomputation. It's an obscure corner-case, but there might be a sequence of steps around a loop that returns to the origin including a taint step that affects the tracked type. In the first application of big-step TC then such a loop is preserved as a step, but a second application removes it, which seems wrong. So I think we should drop this constraint here.
| node1 != node2 |
There was a problem hiding this comment.
Shouldn't the node1 != node2 constraint then also be removed from localFlowStepPlus? Even if a node steps to itself as a taint step, the old type should be compatible with the new type, so I wouldn't expect us to gain much from updating the type.
There was a problem hiding this comment.
Quite possibly. It's certainly corner-case, though.
There was a problem hiding this comment.
#17877 shows the effect of allowing reflexive big steps; I'm not convinced that we want to add it, DCA on this PR also showed no alert changes (the ones for C# are wobble).
There was a problem hiding this comment.
Ok, let's go with the PR as-is, then.
No description provided.