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

[Pip Cet <pipcet@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 1827 bytes --]

On Sun, Feb 21, 2021 at 12:14 AM Mauricio Collares
<mauricio@collares.org> 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.

[-- Attachment #2: 0001-native-comp-Fix-constraint-for-assume-x-and-a-b-Bug-.patch --]
[-- Type: text/x-patch, Size: 902 bytes --]

From bd3a823b827c9394c11aae63dc3fa81098699296 Mon Sep 17 00:00:00 2001
From: Pip Cet <pipcet@gmail.com>
Date: Sun, 21 Feb 2021 11:44:27 +0000
Subject: [PATCH] [native-comp] Fix constraint for (assume x (and a b))
 (Bug#46670)

* lisp/emacs-lisp/comp.el (comp-fwprop-insn): Use comp-cstr-union, not
comp-cstr-intersection.
---
 lisp/emacs-lisp/comp.el | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lisp/emacs-lisp/comp.el b/lisp/emacs-lisp/comp.el
index 4036080976546..965121657f601 100644
--- a/lisp/emacs-lisp/comp.el
+++ b/lisp/emacs-lisp/comp.el
@@ -3059,7 +3059,7 @@ comp-fwprop-insn
     (`(assume ,lval (,kind . ,operands))
      (cl-case kind
        (and
-        (apply #'comp-cstr-intersection lval operands))
+        (apply #'comp-cstr-union lval operands))
        (not
         ;; Prevent double negation!
         (unless (comp-cstr-neg (car operands))
-- 
2.30.0