Subject: Re: bug#65726: 29.1.50; Crash in regexp engine

From: Mattias Engdegård <[email-masked]>
Date: Sat, 16 Sep 2023 12:49:58 +0200

16 sep. 2023 kl. 05.45 skrev Stefan Monnier <[email-masked]>:

>>> (At this point
>>> someone will inevitably point out a helpful invariant that is obvious
>>> in hindsight. This is just my cunning attempt at making that happen.)
> 
> I think I have a "helpful invariant", finally:

Everything is proceeding as I have foreseen.

> Because of how we build our code, when we're at an `on_failure_jump` the
> two branches can either both go forward (typically for a "|" or a "?"),
> or *one* of them goes backward the other forward (for loops), where the
> one that goes backward (i.e. `p2 <= p2_orig`) is the edge (call it
> `p2_loop`) that goes back to the beginning of the loop and the other
> (call it `p2_exit`) is the one that exits the loop.
> 
> Now, because our loops are nested with proper "structured programming",
> there can't be any jump from within the loop to outside the loop except
> for the current jump.  And there can't be any jump from outside the loop
> to inside the loop except by entering via `p2_loop`.
> 
> Since we have two recursive calls to `mutually_exclusive_p` (one for
> `p2_exit` and one for `p2_loop`) and each one only needs to check those
> positions not checked by the other, we can say that `p2_loop` only needs
> to check the positions within the loop (i.e. between `p2_loop` and
> `p2_exit`) and can presume that *all* other positions are checked by the
> other recursive call (the one that starts at `p2_exit`).
> 
> So I think a single arg `done_end` (set, like the current `done_end`, to
> `p2_loop` when recursing into `p2_loop`) is indeed sufficient: there's
> no way to go from `p2_loop` to before `p2_loop` without first going to
> `p2_exit` (which is already checked by the other call).

I think you are right, but wouldn't mind seeing it confirmed empirically. Say, by cross-checking using an an alternative (slower) implementation that directly checks whether a node has been visited before.