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

Previous Next

Full log

View this message in rfc822 format

From: Andrea Corallo <akrl <at> sdf.org>
To: Pip Cet <pipcet <at> gmail.com>
Cc: 46670 <at> debbugs.gnu.org, Mauricio Collares <mauricio <at> collares.org>
Subject: bug#46670: 28.0.50; [feature/native-comp] possible miscompilation affecting lsp-mode
Date: Sun, 21 Feb 2021 21:03:28 +0000

Pip Cet <pipcet <at> gmail.com> writes:

> On Sun, Feb 21, 2021 at 11:51 AM Pip Cet <pipcet <at> gmail.com> 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

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.