Re: feature/native-comp 5bc0855 2/2: Don't treat '=' as simple equality emitting constraints (bug#46812)

Re: feature/native-comp 5bc0855 2/2: Don't treat '=' as simple equality emitting constraints (bug#46812)

[Pip Cet]

On Sun, Feb 28, 2021 at 11:02 PM Andrea Corallo <akrl@savannah.gnu.org> wrote:
> branch: feature/native-comp
> commit 5bc08559e8f171eafc3c034232f8cfd9eaf89862
> Author: Andrea Corallo <akrl@sdf.org>
> Commit: Andrea Corallo <akrl@sdf.org>
>
>     Don't treat '=' as simple equality emitting constraints (bug#46812)
>
>     Extend assumes allowing the following form
>
>     (assume dst (= src1 src2))
>
>     to caputure '=' semanting during fwprop handling float integer
>     conversions.
>
>         * lisp/emacs-lisp/comp.el (comp-equality-fun-p): Don't treat '=' as
>         simple equality.
>         (comp-arithm-cmp-fun-p, comp-negate-arithm-cmp-fun)
>         (comp-reverse-arithm-fun): Rename and add '=' '!='.
>         (comp-emit-assume, comp-add-cond-cstrs, comp-fwprop-insn): Update
>         for new function nameing and to handle '='.
>         * lisp/emacs-lisp/comp-cstr.el (comp-cstr-=): New function.
>         * test/src/comp-tests.el (comp-tests-type-spec-tests): Add a bunch
>         of '=' specific tests.
> ---
>  lisp/emacs-lisp/comp-cstr.el | 12 +++++++++++
>  lisp/emacs-lisp/comp.el      | 37 ++++++++++++++++++++--------------
>  test/src/comp-tests.el       | 47 ++++++++++++++++++++++++++++++++++++++------
>  3 files changed, 75 insertions(+), 21 deletions(-)
>
> diff --git a/lisp/emacs-lisp/comp-cstr.el b/lisp/emacs-lisp/comp-cstr.el
> index 89815f0..bd1e04f 100644
> --- a/lisp/emacs-lisp/comp-cstr.el
> +++ b/lisp/emacs-lisp/comp-cstr.el
> @@ -859,6 +859,18 @@ Non memoized version of `comp-cstr-intersection-no-mem'."
>           (null (neg cstr))
>           (equal (typeset cstr) '(cons)))))
>
> +(defun comp-cstr-= (dst old-dst src)
> +  "Constraint DST being = SRC."
> +  (with-comp-cstr-accessors
> +    (comp-cstr-intersection dst old-dst src)
> +    (cl-loop for v in (valset dst)
> +             when (and (floatp v)
> +                       (= v (truncate v)))
> +               do (push (cons (truncate v) (truncate v)) (range dst)))
> +    (cl-loop for (l . h) in (range dst)
> +             when (eql l h)
> +               do (push (float l) (valset dst)))))

I'm not sure what this is supposed to do: first you form the
intersection of OLD-DST and SRC [often, empty]. Then you iterate over
the values and ranges of the [empty] intersection [leaving it empty].

It's not working either, as far as I can tell: (lambda (x) (and
(floatp x) (= x 0) x)) always returns nil when compiled.

Pip

Re: feature/native-comp 5bc0855 2/2: Don't treat '=' as simple equality emitting constraints (bug#46812)

[Andrea Corallo via Emacs development discussions.]

> It's not working either, as far as I can tell: (lambda (x) (and
> (floatp x) (= x 0) x)) always returns nil when compiled.

Right, I think a better approach is to relax the inputs before
intersecting them so intersection is not cutting off already constrained
inputs.  8c7228e8cd for now follows this conservative approach and adds
some testing for the case.

  Andrea

Re: feature/native-comp 5bc0855 2/2: Don't treat '=' as simple equality emitting constraints (bug#46812)

[Pip Cet]

On Tue, Mar 2, 2021 at 1:47 PM Andrea Corallo <akrl@sdf.org> wrote:
> > It's not working either, as far as I can tell: (lambda (x) (and
> > (floatp x) (= x 0) x)) always returns nil when compiled.
>
> Right, I think a better approach is to relax the inputs before
> intersecting them so intersection is not cutting off already constrained
> inputs.

That should work.

> 8c7228e8cd for now follows this conservative approach and adds
> some testing for the case.

Indeed, and it breaks trying to compile (lambda (x) (unless (= x
1.0e+INF) (error "")) x). (And please don't forget NaNs, they're
numbers too! Except they're not.)

Pip

Re: feature/native-comp 5bc0855 2/2: Don't treat '=' as simple equality emitting constraints (bug#46812)

[Andrea Corallo via Emacs development discussions.]

Pip Cet <pipcet@gmail.com> writes:

> On Tue, Mar 2, 2021 at 1:47 PM Andrea Corallo <akrl@sdf.org> wrote:
>> > It's not working either, as far as I can tell: (lambda (x) (and
>> > (floatp x) (= x 0) x)) always returns nil when compiled.
>>
>> Right, I think a better approach is to relax the inputs before
>> intersecting them so intersection is not cutting off already constrained
>> inputs.
>
> That should work.
>
>> 8c7228e8cd for now follows this conservative approach and adds
>> some testing for the case.
>
> Indeed, and it breaks trying to compile (lambda (x) (unless (= x
> 1.0e+INF) (error "")) x). (And please don't forget NaNs, they're
> numbers too! Except they're not.)

Is there a better way to guard against these cases than catching the
error around truncate?

  Andrea

Re: feature/native-comp 5bc0855 2/2: Don't treat '=' as simple equality emitting constraints (bug#46812)

[Pip Cet]

On Tue, Mar 2, 2021 at 2:30 PM Andrea Corallo <akrl@sdf.org> wrote:
> Pip Cet <pipcet@gmail.com> writes:
> > On Tue, Mar 2, 2021 at 1:47 PM Andrea Corallo <akrl@sdf.org> wrote:
> >> > It's not working either, as far as I can tell: (lambda (x) (and
> >> > (floatp x) (= x 0) x)) always returns nil when compiled.
> >>
> >> Right, I think a better approach is to relax the inputs before
> >> intersecting them so intersection is not cutting off already constrained
> >> inputs.
> >
> > That should work.
> >
> >> 8c7228e8cd for now follows this conservative approach and adds
> >> some testing for the case.
> >
> > Indeed, and it breaks trying to compile (lambda (x) (unless (= x
> > 1.0e+INF) (error "")) x). (And please don't forget NaNs, they're
> > numbers too! Except they're not.)
>
> Is there a better way to guard against these cases than catching the
> error around truncate?

I don't think so, but wrapping it into (float-rational-p) or something
would be nice. Even catching the error, by the way, isn't going to
handle the -0.0 / 0.0 special case properly.

(That is because there is no nice way to handle it, because 0.0 and
-0.0 are the same number and always will be.)

Don't forget this one either (currently miscompiled to have subr-type
((t) nil)):

(lambda (x)
  (unless (= x 0.0) (error ""))
  (unless (eql x -0.0) (error ""))
  x)

There are also some aesthetic issues with how you handle integers too
large to be accurately represented as floats and such, but I'm
focussing on correctness right now.

Pip

Re: feature/native-comp 5bc0855 2/2: Don't treat '=' as simple equality emitting constraints (bug#46812)

[Pip Cet]

On Tue, Mar 2, 2021 at 5:14 PM Pip Cet <pipcet@gmail.com> wrote:
> Don't forget this one either (currently miscompiled to have subr-type
> ((t) nil)):
>
> (lambda (x)
>   (unless (= x 0.0) (error ""))
>   (unless (eql x -0.0) (error ""))
>   x)

That one's still broken.

(lambda (x) (if (eql x 1.0) (error "")) (unless (floatp x) (error "")) x)

is also mis-analyzed to have subr-type (function (t) nil). However,
the compiled code appears to work correctly in both cases. Do you care
about such bugs?

Pip

Re: feature/native-comp 5bc0855 2/2: Don't treat '=' as simple equality emitting constraints (bug#46812)

[Andrea Corallo via Emacs development discussions.]

Pip Cet <pipcet@gmail.com> writes:

> On Tue, Mar 2, 2021 at 5:14 PM Pip Cet <pipcet@gmail.com> wrote:
>> Don't forget this one either (currently miscompiled to have subr-type
>> ((t) nil)):
>>
>> (lambda (x)
>>   (unless (= x 0.0) (error ""))
>>   (unless (eql x -0.0) (error ""))
>>   x)
>
> That one's still broken.
>
> (lambda (x) (if (eql x 1.0) (error "")) (unless (floatp x) (error "")) x)
>
> is also mis-analyzed to have subr-type (function (t) nil). However,
> the compiled code appears to work correctly in both cases. Do you care
> about such bugs?

Indeed I care, but I'm not a full time Emacs developer, I just had no
time to even look into this as ATM I'm busy on other fronts (including
what pays my bills).  Will come back on this as soon as I can.

Thanks

  Andrea

Re: feature/native-comp 5bc0855 2/2: Don't treat '=' as simple equality emitting constraints (bug#46812)

[Andrea Corallo via Emacs development discussions.]

Andrea Corallo via "Emacs development discussions."
<emacs-devel@gnu.org> writes:

> Pip Cet <pipcet@gmail.com> writes:
>
>> On Tue, Mar 2, 2021 at 5:14 PM Pip Cet <pipcet@gmail.com> wrote:
>>> Don't forget this one either (currently miscompiled to have subr-type
>>> ((t) nil)):
>>>
>>> (lambda (x)
>>>   (unless (= x 0.0) (error ""))
>>>   (unless (eql x -0.0) (error ""))
>>>   x)
>>
>> That one's still broken.
>>
>> (lambda (x) (if (eql x 1.0) (error "")) (unless (floatp x) (error "")) x)
>>
>> is also mis-analyzed to have subr-type (function (t) nil). However,
>> the compiled code appears to work correctly in both cases. Do you care
>> about such bugs?
>
> Indeed I care, but I'm not a full time Emacs developer, I just had no
> time to even look into this as ATM I'm busy on other fronts (including
> what pays my bills).  Will come back on this as soon as I can.

The two reported miscompilations should be fixed now as of c60f2f458a,
please have a look.

Still have to look into the missed optimization for the null returning
function, will do.

Thanks

  Andrea

Re: feature/native-comp 5bc0855 2/2: Don't treat '=' as simple equality emitting constraints (bug#46812)

[Pip Cet]

On Sat, Mar 6, 2021 at 10:18 PM Andrea Corallo <akrl@sdf.org> wrote:
> The two reported miscompilations should be fixed now as of c60f2f458a,
> please have a look.

I did. I still don't understand how the intersect-first-then-relax
approach is meant to work, and it's not working.

Here's a more fundamental problem: if we modify two values known to be
equal, they might no longer be:

(let* ((cons1 '(a))
       (cons2 (copy-sequence cons1))
       (cons3 (copy-sequence cons1)))
  (subr-type (native-compile
              `(lambda (x y)
                 (unless (eq x ',cons1)
                   (error ""))
                 (unless (eq y ',cons2)
                   (error ""))
                 (setcar ',cons1 'b)
                 (equal y ',cons3)))))


> Still have to look into the missed optimization for the null returning
> function, will do.

I'm not sure what you're referring to here. My approach, and it's
perfectly okay for you to see this differently, would be to fix the
correctness bugs first, then go for any missed optimizations.

Pip

Re: feature/native-comp 5bc0855 2/2: Don't treat '=' as simple equality emitting constraints (bug#46812)

[Andrea Corallo via Emacs development discussions.]

Pip Cet <pipcet@gmail.com> writes:

[...]

>> Still have to look into the missed optimization for the null returning
>> function, will do.
>
> I'm not sure what you're referring to here.

I was referring to:

Pip Cet <pipcet@gmail.com> writes:

> subr-type (function (t) nil). However, the compiled code appears to
> work correctly in both cases.


  Andrea

Re: feature/native-comp 5bc0855 2/2: Don't treat '=' as simple equality emitting constraints (bug#46812)

[Pip Cet]

On Sun, Mar 7, 2021 at 7:07 AM Andrea Corallo <akrl@sdf.org> wrote:
> Pip Cet <pipcet@gmail.com> writes:
> >> Still have to look into the missed optimization for the null returning
> >> function, will do.
> >
> > I'm not sure what you're referring to here.
>
> I was referring to:
>
> Pip Cet <pipcet@gmail.com> writes:
>
> > subr-type (function (t) nil). However, the compiled code appears to
> > work correctly in both cases.

Oh, okay. I don't think that was a mere missed optimization, claiming
a returning function never returns is bound to cause miscompilation
bugs one day. However, it appears your recent changes have fixed the
cases I'm aware of :-)

Pip