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

[Pip Cet <pipcet@gmail.com>]

Hello Andrea,

On Wed, Feb 24, 2021 at 10:06 AM Andrea Corallo <akrl@sdf.org> wrote:
>
> Pip Cet <pipcet@gmail.com> writes:
>
> > On Wed, Feb 24, 2021 at 9:42 AM Andrea Corallo <akrl@sdf.org> wrote:
> >> (assume #(mvar 22593374 2 (not (integer 3 3))) (not #(mvar 22590962 2 (integer 3 3))))
> >
> > If that doesn't mean "the variable in slot 2 is not equal to the
> > variable in slot 2", we desperately need to work on the LIMPLE
> > syntax...
>
> Honestly I think would be fair from your side to first try to understand
> how it works before criticizing it or submitting untested patches.

I thought I'd give this some time to let tempers cool.

I appreciate your criticism (but not the ad hominem), and I will take
it into account when communicating with you.

I'm sorry you mistook the patches I sent as being submitted for
immediate inclusion: so far, that hasn't been my intention. They're
meant to demonstrate ideas and indicate which area I'm working on.
I'll try to make that clear in future.

As for the immediate issue: LIMPLE, of course, is yours to define as
you wish. If, however, you don't define it, either in documentation or
by providing code that handles it correctly, you can hardly blame me
for considering it a bug if the obvious interpretation causes subtle,
unnecessary problems.

To pick an example at random, after your recent changes, I assumed the
following would be valid LIMPLE (pseudocode):

(set (mvar :slot -1) (mvar :slot 0))

but it's not, because negatively-indexed "temporary variables" aren't
actually mapped to variables in the C backend (instead, they generate
out-of-bounds array accesses, usually a SIGSEGV).

If that is intentional, we need to document it (we also need to assert
rather than segfault when someone disregards this capricious rule) .
If it is unintentional, and I believe it is, do you really want me not
to point it out?

Lastly, on the subject of testing, I believe compiler correctness is
fundamentally more important than not missing any optimizations. Most
of your tests cover the latter aspect.  Maybe we could express that in
the tests somehow, by using another tag?

> Indeed I'm happy to answer as I've explained what this means in my
> previous mail.

I'm not sure I understand that sentence. I'll try looking through
previous messages from you for an explanation, I guess?

> And I've to say, not everything that's not working as you'd expect at
> first glance is broken by definition, this is just not a very good
> collaborative approach :/

My expectations are based, in part, on having read through your code,
including the comments. That's hardly "at first glance".

If I still misunderstand things fundamentally, it's possible, even
likely, that we need to add more documentation (and correct existing
documentation) explaining, for example, that meta-variables introduced
in an assume do not have a value and that their slot number is
meaningless. Once we've done that, we can discuss why I think that
would be a very bad design choice.

Regards
Pip