bug#65726: 29.1.50; Crash in regexp engine

["Mattias Engdegård" <mattias.engdegard@gmail.com>]

5 sep. 2023 kl. 17.33 skrev Stefan Monnier <monnier@iro.umontreal.ca>:

> You can ignore the `mutually_exclusive_(charset|exactn)` thingies which
> just move code around (it's necessary for the patch).

Actually that's a good refactoring to start with regardless of the path we follow later. Makes things more readable if nothing else.

> The basic idea is that `done` points to the beginning of the "current
> loop": as long as we move forward we presume we may still be in the
> current loop, and when we find a jump backward it's either a jump to the
> beginning of a new (nested/further) loop (so we move `done`) or a jump
> to the same loop or to some earlier loop (which we presumably handle
> elsewhere).

So how can we describe the exact semantics of `done` in mutually_exclusive_aux(p1,p2,done)?
Something like:

Let me(p1,p2) = true iff (p1 matches) implies (p2 fails).
Then me_aux(p1,p2,done) = me(p1,p2)
under the assumption that me(p1,x) holds for all x<done where x is reachable from p2.

?

> Adding an `assert (p2 >= done)` confirms that this does happen,

Can you give an example of such a regexp? I ran `make check` with your patch applied and checking enabled but got no assertion failure.

> so
> whether we return true or false when `p2 < done` does matter, so I guess
> we should go with the safer option unless we can really convince
> ourselves that the more optimistic option is also correct.
> 
> Then again, maybe we should bite the bullet and actually keep track of
> the positions already visited, so we don't need any "fancy" argument.

There are a couple of ways of doing that but it might not be that bad. It would also be more robust in face of future changes that may not obey the current invariants.