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

classic Classic list List threaded Threaded
38 messages Options
12
Reply | Threaded
Open this post in threaded view
|

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

Mauricio Collares

This was found by Anthony Cowley, who isolated the exact function in
lsp-mode that was misbehaving. I verified that I could reproduce this
findings, and then I removed surrounding context to obtain a minimized
testcase. If this fails to reproduce, it's entirely my fault.

Steps to reproduce:

1) Put this in minimized.el:

;;; -*- lexical-binding: t; -*-

(defun minimized--look-back (s)
  (and (equal (buffer-substring-no-properties (- (point) (length s)) (point))
              s)
       s))

(defun minimized-go ()
  (interactive)
  (message (minimized--look-back ".")))

(provide 'minimized)

2) Type "." in a buffer and then run minimized-go with the point after
the period. This prints back "." in the minibuffer if the code's
interpreted but not if it's native-compiled.

Note that removing the "lexical-binding: t" line makes the bug not
reproduce. Replacing "(- (point) (length s))" by "(1- (point))" also
makes the bug disappear.

Best,
Mauricio



Reply | Threaded
Open this post in threaded view
|

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

Pip Cet
On Sun, Feb 21, 2021 at 12:14 AM Mauricio Collares
<[hidden email]> wrote:

> This was found by Anthony Cowley, who isolated the exact function in
> lsp-mode that was misbehaving. I verified that I could reproduce this
> findings, and then I removed surrounding context to obtain a minimized
> testcase. If this fails to reproduce, it's entirely my fault.
>
> Steps to reproduce:
>
> 1) Put this in minimized.el:
>
> ;;; -*- lexical-binding: t; -*-
>
> (defun minimized--look-back (s)
>   (and (equal (buffer-substring-no-properties (- (point) (length s)) (point))
>               s)
>        s))
>
> (defun minimized-go ()
>   (interactive)
>   (message (minimized--look-back ".")))
>
> (provide 'minimized)
>
> 2) Type "." in a buffer and then run minimized-go with the point after
> the period. This prints back "." in the minibuffer if the code's
> interpreted but not if it's native-compiled.
>
> Note that removing the "lexical-binding: t" line makes the bug not
> reproduce. Replacing "(- (point) (length s))" by "(1- (point))" also
> makes the bug disappear.
I can reproduce this with this code:

(funcall
 (let ((comp-verbose 3) (comp-debug 3))
   (native-compile `(lambda (s) (and (equal
(buffer-substring-no-properties (- (point) (length s)) (point)) s)
s))))
 ")")

I think there's some confusion in comp-fwprop-insn between (and) as a
logical operator and (and) as a pcase operator. The latter means a
variable's constraint must be in the intersection of all argument
types, but the former only implies that the variable constraint is
somewhere in the union of the argument constraints [1].

Does the attached patch help? Andrea, is my analysis correct?

Pip

[1] - note that we emit (assume a (and b c)) for (setq a (and c b))
under some circumstances, so it would be incorrect to use only c's
constraint.

0001-native-comp-Fix-constraint-for-assume-x-and-a-b-Bug-.patch (1K) Download Attachment
Reply | Threaded
Open this post in threaded view
|

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

Pip Cet
On Sun, Feb 21, 2021 at 11:51 AM Pip Cet <[hidden email]> wrote:
> Does the attached patch help? Andrea, is my analysis correct?

CCing Andrea.

In more detail, some debugging showed we were trying to intersect a
"nil or t" constraint with a "sequence" constraint, the result being a
null constraint (t is not a sequence). So if (assume (and a b)) was
meant to imply the intersection of a and b, we're emitting it
incorrectly.

Pip



Reply | Threaded
Open this post in threaded view
|

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

Emacs - Bugs mailing list
Pip Cet <[hidden email]> writes:

> On Sun, Feb 21, 2021 at 11:51 AM Pip Cet <[hidden email]> wrote:
>> Does the attached patch help? Andrea, is my analysis correct?
>
> CCing Andrea.
>
> In more detail, some debugging showed we were trying to intersect a
> "nil or t" constraint with a "sequence" constraint, the result being a
> null constraint (t is not a sequence). So if (assume (and a b)) was
> meant to imply the intersection of a and b, we're emitting it
> incorrectly.

Hi Pip,

thanks for looking into this.

'and' is meant to imply intersection, so yeah... as you guess there's
some problem in the LIMPLE we generate :)

Just to mention we have also a number of tests in comp-tests.el to
checks that we predict the correct return value, applying the suggested
patch a number of these are not passing.  We'll want to add also a new
test there for this specific case when the issue is solved.

Here a slightly more reduced test-case I'm using here for the analysis
for which the compiler erroneously proves the return type is null.

(let ((comp-verbose 3))
  (native-compile
   '(╬╗ (s)
      (and (equal (foo (length s)) s)
           s))))

Here is why, looking at LIMPLE coming in the final pass in bb_1 we emit:

(assume #(mvar 41121096 0 null) (and #(mvar 42082902 0 sequence) #(mvar 41121566 1 boolean)))

bb_1 is the basic block where 'equal' is verified so we want to enforce
that the result cstr of the call 'foo' is intersected with 's' because
they are equal.

Now the trouble is that while 's' here is represented correctly by the
mvar 42082902 the other operand of the and constraint is wrong.  Where
this is coming from then?

Inside the predecessor block bb_0 we have the compare and branch
sequence:

(set #(mvar 41121566 1 boolean) (call equal #(mvar 42082358 1 t) #(mvar 41665638 2 sequence)))
(cond-jump #(mvar 41121566 1 boolean) #(mvar nil nil null) bb_2_cstrs_0 bb_1)

Here when we run the 'add-cstrs' pass `comp-add-cond-cstrs' is deciding
that 42082358 41665638 must be constrained and therefore is emitting the
assume.  Unfortunatelly because 42082358 and 41121566 are sharing the
same slot number when we do the next SSA rename the mvar referenced in
the assume will be one that is produced by 'equal' and not the one that
is consumed.

The correct fix is to have `comp-add-cond-cstrs' rewrite the comparison
sequence as something like:

(set #(mvar nil X t) #(mvar 42082358 1 t))
(set #(mvar 41121566 1 boolean) (call equal #(mvar 42082358 1 t) #(mvar 41665638 2 sequence)))
(cond-jump #(mvar 41121566 1 boolean) #(mvar nil nil null) bb_2_cstrs_0 bb_1)

Where X is a new slot we add to the frame.  We will reference this slot
number in the assume instead of 1 so it does not get clobbered.

Now I'm not 100% sure how trivial is to do that as no pass is ATM
changing the frame size.

I guess I'll try to write a patch tomorrow evening.

Thanks!

  Andrea



Reply | Threaded
Open this post in threaded view
|

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

Pip Cet
On Sun, Feb 21, 2021 at 9:03 PM Andrea Corallo <[hidden email]> wrote:

> Pip Cet <[hidden email]> writes:
>
> > On Sun, Feb 21, 2021 at 11:51 AM Pip Cet <[hidden email]> wrote:
> >> Does the attached patch help? Andrea, is my analysis correct?
> >
> > CCing Andrea.
> >
> > In more detail, some debugging showed we were trying to intersect a
> > "nil or t" constraint with a "sequence" constraint, the result being a
> > null constraint (t is not a sequence). So if (assume (and a b)) was
> > meant to imply the intersection of a and b, we're emitting it
> > incorrectly.
>
> Hi Pip,
>
> thanks for looking into this.
Thanks for your explanation!

> 'and' is meant to imply intersection, so yeah... as you guess there's
> some problem in the LIMPLE we generate :)

Thanks, I was on the wrong track there.

> The correct fix is to have `comp-add-cond-cstrs' rewrite the comparison
> sequence as something like:
>
> (set #(mvar nil X t) #(mvar 42082358 1 t))
> (set #(mvar 41121566 1 boolean) (call equal #(mvar 42082358 1 t) #(mvar 41665638 2 sequence)))
> (cond-jump #(mvar 41121566 1 boolean) #(mvar nil nil null) bb_2_cstrs_0 bb_1)
>
> Where X is a new slot we add to the frame.  We will reference this slot
> number in the assume instead of 1 so it does not get clobbered.

Okay, I think I understand the problem (we don't do classical SSA and
throw away the slot numbers), and your solution would avoid it, but it
seems needlessly complicated to me.

Why create a new slot that isn't used anywhere? The value of the stack
slot is clobbered by the (set ...), so we cannot emit any assumptions
about that stack slot based on previous values it held.

In fact, all we need to do is tell comp-cond-cstrs-target-mvar to
return nil more often, isn't it?

Pip

0001-Don-t-lie-about-who-set-the-variable.patch (1K) Download Attachment
Reply | Threaded
Open this post in threaded view
|

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

Emacs - Bugs mailing list
Pip Cet <[hidden email]> writes:

> On Sun, Feb 21, 2021 at 9:03 PM Andrea Corallo <[hidden email]> wrote:
>> Pip Cet <[hidden email]> writes:
>>
>> > On Sun, Feb 21, 2021 at 11:51 AM Pip Cet <[hidden email]> wrote:
>> >> Does the attached patch help? Andrea, is my analysis correct?
>> >
>> > CCing Andrea.
>> >
>> > In more detail, some debugging showed we were trying to intersect a
>> > "nil or t" constraint with a "sequence" constraint, the result being a
>> > null constraint (t is not a sequence). So if (assume (and a b)) was
>> > meant to imply the intersection of a and b, we're emitting it
>> > incorrectly.
>>
>> Hi Pip,
>>
>> thanks for looking into this.
>
> Thanks for your explanation!
>
>> 'and' is meant to imply intersection, so yeah... as you guess there's
>> some problem in the LIMPLE we generate :)
>
> Thanks, I was on the wrong track there.
>
>> The correct fix is to have `comp-add-cond-cstrs' rewrite the comparison
>> sequence as something like:
>>
>> (set #(mvar nil X t) #(mvar 42082358 1 t))
>> (set #(mvar 41121566 1 boolean) (call equal #(mvar 42082358 1 t) #(mvar 41665638 2 sequence)))
>> (cond-jump #(mvar 41121566 1 boolean) #(mvar nil nil null) bb_2_cstrs_0 bb_1)
>>
>> Where X is a new slot we add to the frame.  We will reference this slot
>> number in the assume instead of 1 so it does not get clobbered.
>
> Okay, I think I understand the problem (we don't do classical SSA and
> throw away the slot numbers), and your solution would avoid it, but it
> seems needlessly complicated to me.

Correct, ATM the assumption is that we keep LIMPLE always as
"conventional SSA form".  This for a number of reasons but mainly it
greatly helps in maintaining the compiler simple.

I've experimented investing quite some effort into removing this
assumption but the result was definitely more complex and the produced
code considerably harder to debug.  The only advantage I could see in
the end was having a simpler and more elegant
`comp-cond-cstrs-target-mvar' due to the fact that was trivial to
implement a copy propagation pass), so I deemed was a good move to keep
always the conventional form.

> Why create a new slot that isn't used anywhere? The value of the stack
> slot is clobbered by the (set ...), so we cannot emit any assumptions
> about that stack slot based on previous values it held.

Yes but in this case (and probably others) we *have* to emit this
assumption.

The best option is to decide that negative slot numbers are not rendered
into libgccjit IR and we consider these virtual to solve these kind of
cases.  IIRC we already do something similar for the -1 index so this
concept has just to be generalized a bit.

> In fact, all we need to do is tell comp-cond-cstrs-target-mvar to
> return nil more often, isn't it?

Nope, the target mvar identified is the correct one, we just have ATM no
way to reference it reliably into the assume.  BTW applying your patch
is breaking quite some of the comp-tests-ret-type-spec-* tests :)

  Andrea



Reply | Threaded
Open this post in threaded view
|

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

Pip Cet
On Mon, Feb 22, 2021 at 9:38 AM Andrea Corallo <[hidden email]> wrote:

> Pip Cet <[hidden email]> writes:
> > On Sun, Feb 21, 2021 at 9:03 PM Andrea Corallo <[hidden email]> wrote:
> >> Pip Cet <[hidden email]> writes:
> >>
> >> > On Sun, Feb 21, 2021 at 11:51 AM Pip Cet <[hidden email]> wrote:
> >> >> Does the attached patch help? Andrea, is my analysis correct?
> >> >
> >> > CCing Andrea.
> >> >
> >> > In more detail, some debugging showed we were trying to intersect a
> >> > "nil or t" constraint with a "sequence" constraint, the result being a
> >> > null constraint (t is not a sequence). So if (assume (and a b)) was
> >> > meant to imply the intersection of a and b, we're emitting it
> >> > incorrectly.
> >>
> >> Hi Pip,
> >>
> >> thanks for looking into this.
> >
> > Thanks for your explanation!
> >
> >> 'and' is meant to imply intersection, so yeah... as you guess there's
> >> some problem in the LIMPLE we generate :)
> >
> > Thanks, I was on the wrong track there.
> >
> >> The correct fix is to have `comp-add-cond-cstrs' rewrite the comparison
> >> sequence as something like:
> >>
> >> (set #(mvar nil X t) #(mvar 42082358 1 t))
> >> (set #(mvar 41121566 1 boolean) (call equal #(mvar 42082358 1 t) #(mvar 41665638 2 sequence)))
> >> (cond-jump #(mvar 41121566 1 boolean) #(mvar nil nil null) bb_2_cstrs_0 bb_1)
> >>
> >> Where X is a new slot we add to the frame.  We will reference this slot
> >> number in the assume instead of 1 so it does not get clobbered.
> >
> > Okay, I think I understand the problem (we don't do classical SSA and
> > throw away the slot numbers), and your solution would avoid it, but it
> > seems needlessly complicated to me.
>
> Correct, ATM the assumption is that we keep LIMPLE always as
> "conventional SSA form".  This for a number of reasons but mainly it
> greatly helps in maintaining the compiler simple.

"Conventional" meaning "not quite SSA"? I'm just trying to understand,
the decision seems correct to me, since we already ran stack slot
allocation in the byte compiler and we want to reuse those
assignments.

> > Why create a new slot that isn't used anywhere? The value of the stack
> > slot is clobbered by the (set ...), so we cannot emit any assumptions
> > about that stack slot based on previous values it held.
>
> Yes but in this case (and probably others) we *have* to emit this
> assumption.

Why? Are you saying the compiler requires (assume ...) insns for
correctness? If it does, I'm afraid that's a serious issue.

> The best option is to decide that negative slot numbers are not rendered
> into libgccjit IR and we consider these virtual to solve these kind of
> cases.  IIRC we already do something similar for the -1 index so this
> concept has just to be generalized a bit.

Again, that does seem very complicated, and if it improves
optimization we could probably improve it much more by modifying the
byte compiler to pop arguments in the caller rather than the callee.

> > In fact, all we need to do is tell comp-cond-cstrs-target-mvar to
> > return nil more often, isn't it?
>
> Nope, the target mvar identified is the correct one, we just have ATM no
> way to reference it reliably into the assume.

We don't have to, let's just not emit an assume about a variable that
we just introduced and that's never read?

> BTW applying your patch
> is breaking quite some of the comp-tests-ret-type-spec-* tests :)

Where do you keep those?

I see the same number of test failures with and without the patch,
running "make check". The failures seem unrelated, too...



Reply | Threaded
Open this post in threaded view
|

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

Pip Cet
On Mon, Feb 22, 2021 at 10:04 AM Pip Cet <[hidden email]> wrote:

> > BTW applying your patch
> > is breaking quite some of the comp-tests-ret-type-spec-* tests :)
>
> Where do you keep those?

Oh, I see, they're written as though they tested comp.c.

At a quick glance, the test results aren't actually incorrect, they're
merely missed optimizations.

(Except for this one:

      ((defun comp-tests-ret-type-spec-f (x)
         (unless (symbolp x)
           x))
       (not symbol))

If I'm reading that correctly, it tests that (unless (symbolp x) x)
isn't a symbol, which it usually is)



Reply | Threaded
Open this post in threaded view
|

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

Emacs - Bugs mailing list
In reply to this post by Pip Cet
Pip Cet <[hidden email]> writes:

> On Mon, Feb 22, 2021 at 9:38 AM Andrea Corallo <[hidden email]> wrote:
>> Pip Cet <[hidden email]> writes:
>> > On Sun, Feb 21, 2021 at 9:03 PM Andrea Corallo <[hidden email]> wrote:
>> >> Pip Cet <[hidden email]> writes:
>> >>
>> >> > On Sun, Feb 21, 2021 at 11:51 AM Pip Cet <[hidden email]> wrote:
>> >> >> Does the attached patch help? Andrea, is my analysis correct?
>> >> >
>> >> > CCing Andrea.
>> >> >
>> >> > In more detail, some debugging showed we were trying to intersect a
>> >> > "nil or t" constraint with a "sequence" constraint, the result being a
>> >> > null constraint (t is not a sequence). So if (assume (and a b)) was
>> >> > meant to imply the intersection of a and b, we're emitting it
>> >> > incorrectly.
>> >>
>> >> Hi Pip,
>> >>
>> >> thanks for looking into this.
>> >
>> > Thanks for your explanation!
>> >
>> >> 'and' is meant to imply intersection, so yeah... as you guess there's
>> >> some problem in the LIMPLE we generate :)
>> >
>> > Thanks, I was on the wrong track there.
>> >
>> >> The correct fix is to have `comp-add-cond-cstrs' rewrite the comparison
>> >> sequence as something like:
>> >>
>> >> (set #(mvar nil X t) #(mvar 42082358 1 t))
>> >> (set #(mvar 41121566 1 boolean) (call equal #(mvar 42082358 1 t) #(mvar 41665638 2 sequence)))
>> >> (cond-jump #(mvar 41121566 1 boolean) #(mvar nil nil null) bb_2_cstrs_0 bb_1)
>> >>
>> >> Where X is a new slot we add to the frame.  We will reference this slot
>> >> number in the assume instead of 1 so it does not get clobbered.
>> >
>> > Okay, I think I understand the problem (we don't do classical SSA and
>> > throw away the slot numbers), and your solution would avoid it, but it
>> > seems needlessly complicated to me.
>>
>> Correct, ATM the assumption is that we keep LIMPLE always as
>> "conventional SSA form".  This for a number of reasons but mainly it
>> greatly helps in maintaining the compiler simple.
>
> "Conventional" meaning "not quite SSA"? I'm just trying to understand,
> the decision seems correct to me, since we already ran stack slot
> allocation in the byte compiler and we want to reuse those
> assignments.

The SSA book [1] and others discuss conventional and transformed SSA
forms.  IIRC you should find references of these in 2.5 and where copy
propagation is discussed.

>> > Why create a new slot that isn't used anywhere? The value of the stack
>> > slot is clobbered by the (set ...), so we cannot emit any assumptions
>> > about that stack slot based on previous values it held.
>>
>> Yes but in this case (and probably others) we *have* to emit this
>> assumption.
>
> Why? Are you saying the compiler requires (assume ...) insns for
> correctness? If it does, I'm afraid that's a serious issue.

It requires that assume if we want to infer precisely here.  If we
give-up emitting this assume it will just works perfectly but we'll miss
to predict the return value as we should.

>> The best option is to decide that negative slot numbers are not rendered
>> into libgccjit IR and we consider these virtual to solve these kind of
>> cases.  IIRC we already do something similar for the -1 index so this
>> concept has just to be generalized a bit.
>
> Again, that does seem very complicated, and if it improves
> optimization we could probably improve it much more by modifying the
> byte compiler to pop arguments in the caller rather than the callee.

To me this sounds considerably more invasive, probably is because I'm
much more used to work with the native compiler code that with the byte
compiler one :)

I like the idea of the native compiler patch being less invasive as
possible, this was the line I tried to follow and I think so far it
paid.  I guess a number of readers would'd agree with this kind of
approach to begin with.

I think I should be able to work it out as discussed in one two evenings
and it might be useful for other cases in the future too, so it does not
sound as a big deal to me.

>> > In fact, all we need to do is tell comp-cond-cstrs-target-mvar to
>> > return nil more often, isn't it?
>>
>> Nope, the target mvar identified is the correct one, we just have ATM no
>> way to reference it reliably into the assume.
>
> We don't have to, let's just not emit an assume about a variable that
> we just introduced and that's never read?

We disagree :)

We don't need that mvar to render functional code that's agreed, but
still we still need to reference it in the assume (assumes are not
functional code as they are not rendered in final).

As the byte compiler does not care about propagating types and values it
can just clobber the variable, here we aim for more so we need it to
keep it live till the assume.

>> BTW applying your patch
>> is breaking quite some of the comp-tests-ret-type-spec-* tests :)
>
> Where do you keep those?
>
> I see the same number of test failures with and without the patch,
> running "make check". The failures seem unrelated, too...

They are in "test/src/comp-tests.el", those are the first I suggest to
run after having modified the compiler.  Isn't "make check" picking-up
those?

Regards

  Andrea

[1] <http://ssabook.gforge.inria.fr/latest/book.pdf>



Reply | Threaded
Open this post in threaded view
|

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

Emacs - Bugs mailing list
In reply to this post by Pip Cet
Pip Cet <[hidden email]> writes:

> On Mon, Feb 22, 2021 at 10:04 AM Pip Cet <[hidden email]> wrote:
>
>> > BTW applying your patch
>> > is breaking quite some of the comp-tests-ret-type-spec-* tests :)
>>
>> Where do you keep those?
>
> Oh, I see, they're written as though they tested comp.c.
>
> At a quick glance, the test results aren't actually incorrect, they're
> merely missed optimizations.

Correct, note these is not only about potentially missed optimizations,
we expose the derived return type with `subr-type' and in the future we
might give it even more visibility (like using it it in the C-h f
output).

> (Except for this one:
>
>       ((defun comp-tests-ret-type-spec-f (x)
>          (unless (symbolp x)
>            x))
>        (not symbol))
>
> If I'm reading that correctly, it tests that (unless (symbolp x) x)
> isn't a symbol, which it usually is)

Yep, it verifies that this function has as inferred return type (not
symbol).

  Andrea



Reply | Threaded
Open this post in threaded view
|

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

Pip Cet
On Mon, Feb 22, 2021 at 11:23 AM Andrea Corallo <[hidden email]> wrote:

> Pip Cet <[hidden email]> writes:
> > On Mon, Feb 22, 2021 at 10:04 AM Pip Cet <[hidden email]> wrote:
> > (Except for this one:
> >
> >       ((defun comp-tests-ret-type-spec-f (x)
> >          (unless (symbolp x)
> >            x))
> >        (not symbol))
> >
> > If I'm reading that correctly, it tests that (unless (symbolp x) x)
> > isn't a symbol, which it usually is)
>
> Yep, it verifies that this function has as inferred return type (not
> symbol).

Which means the return value shouldn't ever be a symbol, right?
Because it's nil, which is a symbol, when (symbolp x). Am I missing
something here?



Reply | Threaded
Open this post in threaded view
|

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

Emacs - Bugs mailing list
Pip Cet <[hidden email]> writes:

> On Mon, Feb 22, 2021 at 11:23 AM Andrea Corallo <[hidden email]> wrote:
>> Pip Cet <[hidden email]> writes:
>> > On Mon, Feb 22, 2021 at 10:04 AM Pip Cet <[hidden email]> wrote:
>> > (Except for this one:
>> >
>> >       ((defun comp-tests-ret-type-spec-f (x)
>> >          (unless (symbolp x)
>> >            x))
>> >        (not symbol))
>> >
>> > If I'm reading that correctly, it tests that (unless (symbolp x) x)
>> > isn't a symbol, which it usually is)
>>
>> Yep, it verifies that this function has as inferred return type (not
>> symbol).
>
> Which means the return value shouldn't ever be a symbol, right?
> Because it's nil, which is a symbol, when (symbolp x). Am I missing
> something here?

Sorry I though the question was on the test mechanism and wasn't pay
attention to the specific testcase content :/

Right that's clearly a bug in `comp-cstr-union-1-no-mem' that was
missing to check that no negative type is shadowing any positive type
coming from values and giving-up returning t in case).

Good catch thanks! :) Should be fixed by d6227f6edc.

  Andrea

PS as I see you are interested into this part of the compiler, I find
typically handy to exercise this logic with like:

(let ((comp-ctxt (make-comp-cstr-ctxt)))
  (comp-cstr-to-type-spec
   (comp-type-spec-to-cstr '(or (not symbol) null))))

We'll probably see other bugs in this area cause is tricky, is important
we build the best coverage we can for this in the testsuite.



Reply | Threaded
Open this post in threaded view
|

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

Pip Cet
On Mon, Feb 22, 2021 at 1:12 PM Andrea Corallo <[hidden email]> 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.

emacs-bug46670-001.diff (26K) Download Attachment
Reply | Threaded
Open this post in threaded view
|

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

Emacs - Bugs mailing list
Pip Cet <[hidden email]> writes:

> On Mon, Feb 22, 2021 at 1:12 PM Andrea Corallo <[hidden email]> 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



Reply | Threaded
Open this post in threaded view
|

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

Pip Cet
In reply to this post by Emacs - Bugs mailing list
On Mon, Feb 22, 2021 at 11:16 AM Andrea Corallo <[hidden email]> wrote:

> Pip Cet <[hidden email]> writes:
> >> Yes but in this case (and probably others) we *have* to emit this
> >> assumption.
> >
> > Why? Are you saying the compiler requires (assume ...) insns for
> > correctness? If it does, I'm afraid that's a serious issue.
>
> It requires that assume if we want to infer precisely here.  If we
> give-up emitting this assume it will just works perfectly but we'll miss
> to predict the return value as we should.

Emitting an assumption about a dead variable only makes sense if the
dead variable matches a live one. And in that case, we can just emit
the assumption about the live variable to begin with.

> > Again, that does seem very complicated, and if it improves
> > optimization we could probably improve it much more by modifying the
> > byte compiler to pop arguments in the caller rather than the callee.
>
> To me this sounds considerably more invasive, probably is because I'm
> much more used to work with the native compiler code that with the byte
> compiler one :)

That is a little more invasive, but it's where you're going if you
make the major change of allocating your own stack slots rather than
letting the byte compiler do it.

> I like the idea of the native compiler patch being less invasive as
> possible, this was the line I tried to follow and I think so far it
> paid.  I guess a number of readers would'd agree with this kind of
> approach to begin with.

I agree with it! That's why "leave slot allocation to the byte
compiler" is something I don't want you to throw away unnecessarily,
because it's a great simplifying assumption.

> I think I should be able to work it out as discussed in one two evenings
> and it might be useful for other cases in the future too, so it does not
> sound as a big deal to me.

It does to me, I must say. There's nothing special about comparisons:
you're turning a = a OP b two-operand code into c = a OP b
three-operand code. Your code won't be as good as genuine
three-operand code, and it won't be as simple as two-operand code.

> >> > In fact, all we need to do is tell comp-cond-cstrs-target-mvar to
> >> > return nil more often, isn't it?
> >>
> >> Nope, the target mvar identified is the correct one, we just have ATM no
> >> way to reference it reliably into the assume.
> >
> > We don't have to, let's just not emit an assume about a variable that
> > we just introduced and that's never read?
>
> We disagree :)

We can disagree about the "let's" part (and should, of course), but we
should agree about the "we don't have to" part, because that's a
matter of fact, not opinion.

> As the byte compiler does not care about propagating types and values it
> can just clobber the variable, here we aim for more so we need it to
> keep it live till the assume.

If we decide the variable needs to be kept live, the byte compiler
should keep it live, not us.



Reply | Threaded
Open this post in threaded view
|

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

Pip Cet
In reply to this post by Emacs - Bugs mailing list
On Mon, Feb 22, 2021 at 1:12 PM Andrea Corallo <[hidden email]> wrote:
> We'll probably see other bugs in this area cause is tricky, is important
> we build the best coverage we can for this in the testsuite.

Is this one of them, or am I confused?

0001-Don-t-emit-incorrect-assumptions-for-non-equality-Bu.patch (1K) Download Attachment
Reply | Threaded
Open this post in threaded view
|

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

Emacs - Bugs mailing list
In reply to this post by Pip Cet
Pip Cet <[hidden email]> writes:

> On Mon, Feb 22, 2021 at 11:16 AM Andrea Corallo <[hidden email]> wrote:
>> Pip Cet <[hidden email]> writes:
>> >> Yes but in this case (and probably others) we *have* to emit this
>> >> assumption.
>> >
>> > Why? Are you saying the compiler requires (assume ...) insns for
>> > correctness? If it does, I'm afraid that's a serious issue.
>>
>> It requires that assume if we want to infer precisely here.  If we
>> give-up emitting this assume it will just works perfectly but we'll miss
>> to predict the return value as we should.
>
> Emitting an assumption about a dead variable only makes sense if the
> dead variable matches a live one. And in that case, we can just emit
> the assumption about the live variable to begin with.
>
>> > Again, that does seem very complicated, and if it improves
>> > optimization we could probably improve it much more by modifying the
>> > byte compiler to pop arguments in the caller rather than the callee.
>>
>> To me this sounds considerably more invasive, probably is because I'm
>> much more used to work with the native compiler code that with the byte
>> compiler one :)
>
> That is a little more invasive, but it's where you're going if you
> make the major change of allocating your own stack slots rather than
> letting the byte compiler do it.
>
>> I like the idea of the native compiler patch being less invasive as
>> possible, this was the line I tried to follow and I think so far it
>> paid.  I guess a number of readers would'd agree with this kind of
>> approach to begin with.
>
> I agree with it! That's why "leave slot allocation to the byte
> compiler" is something I don't want you to throw away unnecessarily,
> because it's a great simplifying assumption.
>
>> I think I should be able to work it out as discussed in one two evenings
>> and it might be useful for other cases in the future too, so it does not
>> sound as a big deal to me.
>
> It does to me, I must say. There's nothing special about comparisons:
> you're turning a = a OP b two-operand code into c = a OP b
> three-operand code. Your code won't be as good as genuine
> three-operand code, and it won't be as simple as two-operand code.
>
>> >> > In fact, all we need to do is tell comp-cond-cstrs-target-mvar to
>> >> > return nil more often, isn't it?
>> >>
>> >> Nope, the target mvar identified is the correct one, we just have ATM no
>> >> way to reference it reliably into the assume.
>> >
>> > We don't have to, let's just not emit an assume about a variable that
>> > we just introduced and that's never read?
>>
>> We disagree :)
>
> We can disagree about the "let's" part (and should, of course), but we
> should agree about the "we don't have to" part, because that's a
> matter of fact, not opinion.

This new mvar *is* used, actually by an assume.  And the assume in
discussion is targetting a live variable that will be used by functional
code so I really see no scandal here.

>> As the byte compiler does not care about propagating types and values it
>> can just clobber the variable, here we aim for more so we need it to
>> keep it live till the assume.
>
> If we decide the variable needs to be kept live, the byte compiler
> should keep it live, not us.

Again no, any pass in the compiler must have the right to create new
temporaries for whichever purpose it wants, and indeed we can't expect
the byte-compiler to know in advance all passes in the native compiler
and their scopes and goals.  `add-cstrs' is just the first pass that now
happen to have this need, is not a special case of any sort.

Not giving the possibilities to passes to create variables would be
totally equivalent to prevent GIMPLE passes in GCC to create new local
variables while performing transformations, it would be ludicrous and
this is just something we *want* to be able to do.

  Andrea



Reply | Threaded
Open this post in threaded view
|

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

Emacs - Bugs mailing list
In reply to this post by Emacs - Bugs mailing list
Andrea Corallo via "Bug reports for GNU Emacs, the Swiss army knife of
text editors" <[hidden email]> writes:

[...]

> 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

Right I've pushed bddd7a2d13 implementing the discussed solution as I'm
convinced is more general and future proof.

The patch is passing the tests and bootstrapping clean, also is adding a
test that should cover this specific bug.

Mauricio could you verify it actually solves the lsp-mode issue?

Thanks

  Andrea



Reply | Threaded
Open this post in threaded view
|

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

Mauricio Collares


On February 23, 2021 8:26:25 PM GMT-03:00, Andrea Corallo <[hidden email]> wrote:

>Andrea Corallo via "Bug reports for GNU Emacs, the Swiss army knife of
>text editors" <[hidden email]> writes:
>
>Right I've pushed bddd7a2d13 implementing the discussed solution as I'm
>convinced is more general and future proof.
>
>The patch is passing the tests and bootstrapping clean, also is adding a
>test that should cover this specific bug.
>
>Mauricio could you verify it actually solves the lsp-mode issue?

Hi Andrea,

I've verified that the lsp-mode completion issue is fixed. Many, many thanks!

By the way, I just noticed that this is probably the same issue that was reported by X L and Óscar Fuentes in emacs-devel ('Completion doesn't start after "." Is pressed in go-mode with gopls').

Best,
Mauricio



Reply | Threaded
Open this post in threaded view
|

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

Pip Cet
In reply to this post by Pip Cet
On Wed, Feb 24, 2021 at 9:04 AM Andrea Corallo <[hidden email]> wrote:

> Pip Cet <[hidden email]> writes:
>
> > On Tue, Feb 23, 2021 at 11:36 PM Andrea Corallo <[hidden email]> wrote:
> >> Pip Cet <[hidden email]> writes:
> >> > Is this one of them, or am I confused?
> >>
> >> What's suspitions with that?  At present I'm admittedly quite done but
> >> it looks okay to me.
> >
> > We're emitting
> >
> > (assume ,lhs (and ,lhs ,rhs))
> >
> > even when NEGATED is t.
>
> Nope, when NEGATED is t the complete sequence we are emitting is (see
> line just following your diff hunk):
>
> (assume tmp-mvar (not rhs))
But tmp-mvar is in the same slot as RHS.

> (assume lhs (and lhs tmp-mvar))

So this is equivalent (after the next SSA rename) to

(assume lhs (and lhs rhs))

> That's indeed the reason why it's working in the 39 testcases.

No, the reason it's "working" is that we never assert our assumes.
I've got a patch here that does just that :-)

0001-Assert-at-runtime-that-assume-s-assumptions-actually.patch (7K) Download Attachment
12