bug#46670: 28.0.50; [feature/native-comp] possible miscompilation affecting lsp-mode

[Andrea Corallo via "Bug reports for GNU Emacs, the Swiss army knife of text editors" <bug-gnu-emacs@gnu.org>]

Pip Cet <pipcet@gmail.com> writes:

> On Mon, Feb 22, 2021 at 1:12 PM Andrea Corallo <akrl@sdf.org> wrote:
>> Good catch thanks! :) Should be fixed by d6227f6edc.
>
> I'm also confused by the use of NEGATED in comp-emit-assume: if RHS is
> a constraint, it emits the complementary constraint.
>
> However, the code in comp-add-cond-cstrs uses NEGATED to express a
> much weaker constraint: that two mvars aren't strictly equal.
>
> If x /= y and y in SET, we can't conclude that x not in SET (unless
> SET is a singleton, an important special case).
>
> So it all works right now because emit-assume NEGATED=t RHS=mvar means
> "LHS isn't equal to RHS" but NEGATED=t RHS=cstr means "LHS can't
> satisfy RHS".
>
> My code changed the call to pass a constraint instead of the mvar, and
> then things broke :-)
>
> We should be consistent about what NEGATED means, I think.
>
> But apart from such problems, my code appears to be working. I'm
> attaching it for the sake of completeness, not because I expect you to
> read it all before it's cleaned up.

Hi Pip thanks for the patch,

the approach of adding a cstr directly in the assume works for this case
but is not generic as referencing there an mvar.

The reason is that a later run of fw-prop after add-cstrs might be able
to prove more precisely what the mvar is if the code was morphed in the
meanwhile by some other pass.  This in contrast with adding a cstr that
being "written into the stone" will stay as such no matter what.

Admittedly ATM the only pass rewriting some code after assumes are
placed and before the last fw-prop is run is 'tco' so this might be a
real case only for functions affected by this, but in the future we may
(and most likely want to) have more passes in that position of the
compiler pipeline.

So yeah I still prefer to general approach of keeping an mvar live till
there and referencing it in the assume so that any future propagation
within the SSA lattice can update this.

Yesterday evening I did some work in that direction, doesn't look too
invasive or complex.  I'll finish it this week as soon as I've some more
time to put into.

Thanks

  Andrea