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

[Pip Cet <pipcet@gmail.com>]

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

On Mon, Feb 22, 2021 at 1:12 PM Andrea Corallo <akrl@sdf.org> 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.

[-- Attachment #2: emacs-bug46670-001.diff --]
[-- Type: text/x-patch, Size: 19487 bytes --]

diff --git a/lisp/emacs-lisp/comp.el b/lisp/emacs-lisp/comp.el
index 60c040926e54c..3cb7812b5a874 100644
--- a/lisp/emacs-lisp/comp.el
+++ b/lisp/emacs-lisp/comp.el
@@ -690,6 +690,16 @@ comp-args-base
              :documentation "This is a copy of the frame when leaving the block.
 Is in use to help the SSA rename pass."))
 
+(defun comp-block-insns-reverse (bb &optional start)
+  "Return the insns in BB in reverse order, starting with the one before
+START."
+  (let ((insns (comp-block-insns bb))
+        res)
+    (while (not (eq (car insns) start))
+      (push (car insns) res)
+      (setq insns (cdr insns)))
+    res))
+
 (cl-defstruct (comp-block-lap (:copier nil)
                               (:include comp-block)
                               (:constructor make--comp-block-lap
@@ -826,7 +836,7 @@ comp-mvar-value-vld-p
 (defun comp-mvar-value (mvar)
   "Return the constant value of MVAR.
 `comp-mvar-value-vld-p' *must* be satisfied before calling
-`comp-mvar-const'."
+`comp-mvar-value'."
   (declare (gv-setter
             (lambda (val)
               `(if (integerp ,val)
@@ -903,6 +913,10 @@ comp-assign-op-p
   "Assignment predicate for OP."
   (when (memq op comp-limple-assignments) t))
 
+(defun comp-clobbering-assign-op-p (op)
+  "Test if OP is a clobbering assignment."
+  (and (comp-assign-op-p op) (not (eq op 'assume))))
+
 (defun comp-call-op-p (op)
   "Call predicate for OP."
   (when (memq op comp-limple-calls) t))
@@ -2202,7 +2216,7 @@ comp-limplify
 
 
 (defsubst comp-mvar-used-p (mvar)
-  "Non-nil when MVAR is used as lhs in the current funciton."
+  "Non-nil when MVAR is used as rhs in the current function."
   (declare (gv-setter (lambda (val)
 			`(puthash ,mvar ,val comp-pass))))
   (gethash mvar comp-pass))
@@ -2217,7 +2231,7 @@ comp-collect-mvars
                do (setf (comp-mvar-used-p x) t)))
 
 (defun comp-collect-rhs ()
-  "Collect all lhs mvars into `comp-pass'."
+  "Collect all rhs mvars into `comp-pass'."
   (cl-loop
    for b being each hash-value of (comp-func-blocks comp-func)
    do (cl-loop
@@ -2245,7 +2259,14 @@ comp-reverse-cmp-fun
     (<= '>=)
     (t function)))
 
-(defun comp-emit-assume (kind lhs rhs bb negated)
+(defun comp-cstr-singleton-p (cstr)
+  (or (and (comp-cstr-valset cstr)
+           (length= (comp-cstr-valset cstr) 1))
+      (and (comp-cstr-range cstr)
+           (equal (car (comp-cstr-range cstr))
+                  (cdr (comp-cstr-range cstr))))))
+
+(defun comp-emit-assume (kind lhs rhs bb negated &optional strictly)
   "Emit an assume of kind KIND for mvar LHS being RHS.
 When NEGATED is non-nil the assumption is negated.
 The assume is emitted at the beginning of the block BB."
@@ -2253,6 +2274,7 @@ comp-emit-assume
     (cl-assert lhs-slot)
     (pcase kind
       ('and
+       (comp-log (format "assuming4 %S %S %S" lhs rhs negated))
        (if (comp-mvar-p rhs)
            (let ((tmp-mvar (if negated
                                (make-comp-mvar :slot (comp-mvar-slot rhs))
@@ -2263,29 +2285,47 @@ comp-emit-assume
              (if negated
                  (push `(assume ,tmp-mvar (not ,rhs))
 	               (comp-block-insns bb))))
-         ;; If is only a constraint we can negate it directly.
-         (push `(assume ,(make-comp-mvar :slot lhs-slot)
-                        (and ,lhs ,(if negated
-                                       (comp-cstr-negation-make rhs)
-                                     rhs)))
-	       (comp-block-insns bb))))
+         ;; If RHS is a constraint we can negate it directly.
+         (comp-log (format "assuming3 %S %S" lhs rhs))
+         (when (or strictly (not negated))
+           (push `(assume ,(make-comp-mvar :slot lhs-slot)
+                          (and ,lhs ,(if negated
+                                         (comp-cstr-negation-make rhs)
+                                       rhs)))
+	         (comp-block-insns bb)))))
       ((pred comp-range-cmp-fun-p)
-       (let ((kind (if negated
-                       (comp-negate-range-cmp-fun kind)
-                     kind)))
-         (push `(assume ,(make-comp-mvar :slot lhs-slot)
-                        (,kind ,lhs
-                               ,(if-let* ((vld (comp-mvar-value-vld-p rhs))
-                                          (val (comp-mvar-value rhs))
-                                          (ok (integerp val)))
-                                    val
-                                  (make-comp-mvar :slot (comp-mvar-slot rhs)))))
-	       (comp-block-insns bb))))
+       (when (or strictly (not negated) (comp-mvar-p rhs)
+                   (comp-cstr-singleton-p rhs))
+         (let ((kind (if negated
+                         (comp-negate-range-cmp-fun kind)
+                       kind)))
+           (comp-log (format "assuming2 %S %S" lhs rhs))
+           (push `(assume ,(make-comp-mvar :slot lhs-slot)
+                          (,kind ,lhs
+                                 ,(if (comp-mvar-p rhs)
+                                      (if-let* ((vld (comp-mvar-value-vld-p rhs))
+                                                (val (comp-mvar-value rhs))
+                                                (ok (integerp val)))
+                                          val
+                                        (make-comp-mvar :slot (comp-mvar-slot rhs)))
+                                    (comp-cstr-copy rhs))))
+	         (comp-block-insns bb)))))
       (_ (cl-assert nil)))
     (setf (comp-func-ssa-status comp-func) 'dirty)))
 
+(defun comp-emit-assumes (kind lhsl rhsl basic-block negated &optional strictly)
+  "Emit assume insns stating that all elements of LHSL relate to
+all elements of RHSL as KIND, which may be NEGATED.  The insns
+ara added to BASIC-BLOCK."
+  (comp-log (format "assumes %S %S" lhsl rhsl))
+  (dolist (lhs lhsl)
+    (and (comp-mvar-p lhs)
+         (comp-mvar-slot lhs)
+         (dolist (rhs rhsl)
+           (comp-emit-assume kind lhs rhs basic-block negated strictly)))))
+
 (defun comp-add-new-block-between (bb-symbol bb-a bb-b)
-  "Create a new basic-block named BB-SYMBOL and add it between BB-A and BB-B."
+  "Create a new basic block named BB-SYMBOL and add it between BB-A and BB-B."
   (cl-loop
    with new-bb = (make-comp-block-cstr :name bb-symbol
                                        :insns `((jump ,(comp-block-name bb-b))))
@@ -2305,24 +2345,84 @@ comp-add-new-block-between
    ;; Add `new-edge' to the current function and return it.
    (cl-return (puthash bb-symbol new-bb (comp-func-blocks comp-func)))
    finally (cl-assert nil)))
-
-;; Cheap substitute to a copy propagation pass...
-(defun comp-cond-cstrs-target-mvar (mvar exit-insn bb)
-  "Given MVAR search in BB the original mvar MVAR got assigned from.
-Keep on searching till EXIT-INSN is encountered."
-  (cl-flet ((targetp (x)
-              ;; Ret t if x is an mvar and target the correct slot number.
-              (and (comp-mvar-p x)
-                   (eql (comp-mvar-slot mvar) (comp-mvar-slot x)))))
-    (cl-loop
-     with res = nil
-     for insn in (comp-block-insns bb)
-     when (eq insn exit-insn)
-     do (cl-return (and (comp-mvar-p res) res))
-     do (pcase insn
-          (`(,(pred comp-assign-op-p) ,(pred targetp) ,rhs)
-           (setf res rhs)))
-     finally (cl-assert nil))))
+;; "Cheap" substitute for a copy propagation pass...
+(defun comp-cond-cstrs-identical-vars (mvars bb insn)
+  "Search BB for mvars known to be `eq' to all of the MVARS at the time INSN
+is executed."
+  (cl-assert (cl-every #'comp-mvar-p mvars))
+  (cl-loop
+   with slots = (delq nil (mapcar #'comp-mvar-slot mvars))
+   with res = (copy-sequence mvars)
+   with clobbered = nil
+   for insn in (comp-block-insns-reverse bb insn)
+   do (progn
+        (comp-log (format "insn %S slots %S res %S clobbered %S"
+                          insn slots res clobbered))
+        (pcase insn
+        (`(,(and op (pred comp-assign-op-p))
+           ,(and (pred comp-mvar-p) (pred comp-mvar-slot) lhs)
+           ,(and (pred comp-mvar-p) (pred comp-mvar-slot) rhs))
+         (let ((lhs-p (member (comp-mvar-slot lhs) slots))
+               (rhs-p (member (comp-mvar-slot rhs) slots)))
+           (and lhs-p (not rhs-p)
+                (push (comp-mvar-slot rhs) slots)
+                (unless (or (member (comp-mvar-slot lhs) clobbered)
+                            (memq rhs res))
+                  (push rhs res)))
+           (and rhs-p (not lhs-p)
+                (push (comp-mvar-slot lhs) slots)
+                (unless (or (member (comp-mvar-slot rhs) clobbered)
+                            (memq lhs res))
+                  (push lhs res)))
+           (and (comp-clobbering-assign-op-p op)
+                (not lhs-p)
+                (not rhs-p)
+                (setq slots (delete (comp-mvar-slot lhs) slots))
+                (unless (member (comp-mvar-slot lhs) clobbered)
+                  (push (comp-mvar-slot lhs) clobbered))))
+         (comp-log (format "post insn %S slots %S res %S clobbered %S"
+                           insn slots res clobbered)))
+        (`(,(pred comp-clobbering-assign-op-p)
+           ,(and (pred comp-mvar-slot) lhs)
+           _)
+         (unless (member (comp-mvar-slot lhs) clobbered)
+           (push (comp-mvar-slot lhs) clobbered))
+         (setq slots (delete (comp-mvar-slot lhs) slots)))))
+   finally (progn
+             (cl-return res))))
+
+;; "Cheap" substitute for a copy propagation pass...
+(defun comp-cond-cstrs-identical-vars-byvar (mvars bb insn)
+  "Search BB for mvars known to be `eq' to all of the MVARS at the time INSN
+is executed. Exclude the MVARS themselves from the result."
+  (cl-assert (cl-every #'comp-mvar-p mvars))
+  (cl-loop
+   with vars = (copy-sequence mvars)
+   with res = nil
+   with clobbered = nil
+   for insn in (comp-block-insns-reverse bb insn)
+   do (pcase insn
+        (`(,(and op (pred comp-assign-op-p))
+           ,lhs
+           ,(and (pred comp-mvar-p) rhs))
+         (let ((lhs-p (memq lhs vars))
+               (rhs-p (memq rhs vars)))
+           (cond
+            ((and (not lhs-p) rhs-p)
+             (push lhs vars)
+             (unless (or (memq lhs clobbered)
+                         (memq lhs res))
+               (push lhs res)))
+            ((or rhs-p (not (comp-clobbering-assign-op-p op))))
+            ((setq vars (delq lhs vars))
+             (unless (memq lhs clobbered) (push lhs clobbered))))))
+        (`(,(pred comp-clobbering-assign-op-p) ,lhs _)
+         (unless (memq lhs clobbered) (push lhs clobbered))
+         (setq vars (delq lhs vars))))
+   finally (progn
+             (comp-log (format "mvars %S res %S"
+                               mvars res))
+             (cl-return res))))
 
 (defun comp-add-cond-cstrs-target-block (curr-bb target-bb-sym)
   "Return the appropriate basic block to add constraint assumptions into.
@@ -2401,23 +2501,44 @@ comp-add-cond-cstrs
 	 ;; (comment ,_comment-str)
 	 (cond-jump ,cmp-res ,(pred comp-mvar-p) . ,blocks))
        (cl-loop
-        with target-mvar1 = (comp-cond-cstrs-target-mvar op1 (car insns-seq) b)
-        with target-mvar2 = (comp-cond-cstrs-target-mvar op2 (car insns-seq) b)
+        with target-mvars1 = (comp-cond-cstrs-identical-vars
+                               (list op1) b (car insns-seq))
+        with target-mvars2 = (comp-cond-cstrs-identical-vars
+                               (list op2) b (car insns-seq))
         with equality = (comp-equality-fun-p fun)
         for branch-target-cell on blocks
         for branch-target = (car branch-target-cell)
         for negated in '(t nil)
         for kind = (if equality 'and fun)
-        when (or (comp-mvar-used-p target-mvar1)
-                 (comp-mvar-used-p target-mvar2))
         do
+        (comp-log (format "target mvars %S %S"
+                          target-mvars1 target-mvars2))
+        (setq target-mvars1
+              (mapcar
+               (lambda (mvar)
+                 (if (and
+                      (comp-mvar-p mvar)
+                      (equal (comp-mvar-slot mvar)
+                             (comp-mvar-slot cmp-res)))
+                     (comp-cstr-copy mvar)
+                   mvar))
+               target-mvars1))
+        (setq target-mvars2
+              (mapcar
+               (lambda (mvar)
+                 (if (and
+                      (comp-mvar-p mvar)
+                      (equal (comp-mvar-slot mvar)
+                             (comp-mvar-slot cmp-res)))
+                     (comp-cstr-copy mvar)
+                   mvar))
+               target-mvars2))
         (let ((block-target (comp-add-cond-cstrs-target-block b branch-target)))
           (setf (car branch-target-cell) (comp-block-name block-target))
-          (when (comp-mvar-used-p target-mvar1)
-            (comp-emit-assume kind target-mvar1 op2 block-target negated))
-          (when (comp-mvar-used-p target-mvar2)
-            (comp-emit-assume (comp-reverse-cmp-fun kind)
-                              target-mvar2 op1 block-target negated)))
+          (comp-emit-assumes kind
+                             target-mvars1 target-mvars2 block-target negated)
+          (comp-emit-assumes (comp-reverse-cmp-fun kind)
+                             target-mvars2 target-mvars1 block-target negated))
         finally (cl-return-from in-the-basic-block)))
       (`((set ,(and (pred comp-mvar-p) cmp-res)
               (,(pred comp-call-op-p)
@@ -2426,16 +2547,26 @@ comp-add-cond-cstrs
 	 ;; (comment ,_comment-str)
 	 (cond-jump ,cmp-res ,(pred comp-mvar-p) . ,blocks))
        (cl-loop
-        with target-mvar = (comp-cond-cstrs-target-mvar op (car insns-seq) b)
+        with target-mvars = (comp-cond-cstrs-identical-vars
+                             (list op) b (car insns-seq))
         with cstr = (comp-pred-to-cstr fun)
         for branch-target-cell on blocks
         for branch-target = (car branch-target-cell)
         for negated in '(t nil)
-        when (comp-mvar-used-p target-mvar)
+        when target-mvars
         do
+        (setq target-mvars
+              (mapcar (lambda (mvar)
+                        (if (and
+                             (comp-mvar-p mvar)
+                             (equal (comp-mvar-slot mvar)
+                                    (comp-mvar-slot cmp-res)))
+                            (comp-cstr-copy mvar)
+                          mvar))
+                      target-mvars))
         (let ((block-target (comp-add-cond-cstrs-target-block b branch-target)))
           (setf (car branch-target-cell) (comp-block-name block-target))
-          (comp-emit-assume 'and target-mvar cstr block-target negated))
+          (comp-emit-assumes 'and target-mvars (list cstr) block-target negated t))
         finally (cl-return-from in-the-basic-block)))
       ;; Match predicate on the negated branch (unless).
       (`((set ,(and (pred comp-mvar-p) cmp-res)
@@ -2445,16 +2576,27 @@ comp-add-cond-cstrs
          (set ,neg-cmp-res (call eq ,cmp-res ,(pred comp-cstr-null-p)))
 	 (cond-jump ,neg-cmp-res ,(pred comp-mvar-p) . ,blocks))
        (cl-loop
-        with target-mvar = (comp-cond-cstrs-target-mvar op (car insns-seq) b)
+        with target-mvars = (comp-cond-cstrs-identical-vars
+                             (list op) b (car insns-seq))
         with cstr = (comp-pred-to-cstr fun)
         for branch-target-cell on blocks
         for branch-target = (car branch-target-cell)
         for negated in '(nil t)
-        when (comp-mvar-used-p target-mvar)
+        when target-mvars
         do
+        (setq target-mvars
+              (mapcar
+               (lambda (mvar)
+                 (if (and
+                      (comp-mvar-p mvar)
+                      (equal (comp-mvar-slot mvar)
+                             (comp-mvar-slot cmp-res)))
+                     (comp-cstr-copy mvar)
+                   mvar))
+               target-mvars))
         (let ((block-target (comp-add-cond-cstrs-target-block b branch-target)))
           (setf (car branch-target-cell) (comp-block-name block-target))
-          (comp-emit-assume 'and target-mvar cstr block-target negated))
+          (comp-emit-assumes 'and target-mvars (list cstr) block-target negated t))
         finally (cl-return-from in-the-basic-block)))))))
 
 (defsubst comp-insert-insn (insn insn-cell)
@@ -2465,13 +2607,14 @@ comp-insert-insn
           (cdr new-cell) next-cell
           (comp-func-ssa-status comp-func) 'dirty)))
 
-(defun comp-emit-call-cstr (mvar call-cell cstr)
+(defun comp-emit-call-cstrs (mvars call-cell cstr)
   "Emit a constraint CSTR for MVAR after CALL-CELL."
-  (let* ((new-mvar (make-comp-mvar :slot (comp-mvar-slot mvar)))
-         ;; Have new-mvar as LHS *and* RHS to ensure monotonicity and
-         ;; fwprop convergence!!
-         (insn `(assume ,new-mvar (and ,new-mvar ,mvar ,cstr))))
-    (comp-insert-insn insn call-cell)))
+  (dolist (mvar (cl-remove-if-not #'comp-mvar-p mvars))
+    (let* ((new-mvar (make-comp-mvar :slot (comp-mvar-slot mvar)))
+           ;; Have new-mvar as LHS *and* RHS to ensure monotonicity and
+           ;; fwprop convergence!!
+           (insn `(assume ,new-mvar (and ,new-mvar ,mvar ,cstr))))
+      (comp-insert-insn insn call-cell))))
 
 (defun comp-lambda-list-gen (lambda-list)
   "Return a generator to iterate over LAMBDA-LIST."
@@ -2508,18 +2651,24 @@ comp-add-call-cstr
           with gen = (comp-lambda-list-gen (comp-cstr-f-args cstr-f))
           for arg in args
           for cstr = (funcall gen)
-          for target = (comp-cond-cstrs-target-mvar arg insn bb)
+          for target-vars = (comp-cond-cstrs-identical-vars (list arg) bb insn)
           unless (comp-cstr-p cstr)
             do (signal 'native-ice
                        (list "Incoherent type specifier for function" f))
-          when (and target
+          do (setq target-vars (mapcar
+                                (lambda (mvar)
+                                  (if (and
+                                       (comp-mvar-p mvar)
+                                       (equal (comp-mvar-slot mvar)
+                                              (comp-mvar-slot lhs)))
+                                      (comp-cstr-copy mvar)
+                                    mvar))
+                                target-vars))
+          when (and target-vars
                     ;; No need to add call constraints if this is t
                     ;; (bug#45812 bug#45705 bug#45751).
-                    (not (equal comp-cstr-t cstr))
-                    (or (null lhs)
-                        (not (eql (comp-mvar-slot lhs)
-                                  (comp-mvar-slot target)))))
-            do (comp-emit-call-cstr target insn-cell cstr)))))))
+                    (not (equal comp-cstr-t cstr)))
+            do (comp-emit-call-cstrs target-vars insn-cell cstr)))))))
 
 (defun comp-add-cstrs (_)
   "Rewrite conditional branches adding appropriate 'assume' insns.
@@ -2529,7 +2678,7 @@ comp-add-cstrs
   (maphash (lambda (_ f)
              (when (and (>= (comp-func-speed f) 1)
                         ;; No point to run this on dynamic scope as
-                        ;; this pass is effecive only on local
+                        ;; this pass is effective only on local
                         ;; variables.
 			(comp-func-l-p f)
                         (not (comp-func-has-non-local f)))