From 40f4fc1d8c5de4348dc3e9f645d0897f586de2c3 Mon Sep 17 00:00:00 2001
From: Andrea Corallo <acorallo@gnu.org>
Date: Wed, 11 Mar 2026 16:54:46 +0100
Subject: [PATCH] Fix negated equality assumptions (bug#80327)

* lisp/emacs-lisp/comp.el (comp--add-cond-cstrs): Skip
negated equality assumptions only for relational non-immediate
operands. Keep immediate false-branch constraints.
* test/src/comp-resources/comp-test-funcs.el
(comp-test-80327-hash, comp-test-80327-f): Add reproducer.
* test/src/comp-tests.el (comp-tests-bug-80327): Add regression
test.
---
 lisp/emacs-lisp/comp.el                    | 20 ++++++++++++++++----
 test/src/comp-resources/comp-test-funcs.el | 14 ++++++++++++++
 test/src/comp-tests.el                     |  4 ++++
 3 files changed, 34 insertions(+), 4 deletions(-)

diff --git a/lisp/emacs-lisp/comp.el b/lisp/emacs-lisp/comp.el
index 76ad4090bef..f2411d44862 100644
--- a/lisp/emacs-lisp/comp.el
+++ b/lisp/emacs-lisp/comp.el
@@ -2049,24 +2049,36 @@ TARGET-BB-SYM is the symbol name of the target block."
         for branch-target-cell on blocks
         for branch-target = (car branch-target-cell)
         for negated in '(t nil)
+        for eq-fun = (comp--equality-fun-p fun)
+        for op1-imm = (and (comp-cstr-p op1) (comp-cstr-imm-vld-p op1))
+        for op2-imm = (and (comp-cstr-p op2) (comp-cstr-imm-vld-p op2))
+        ;; On a false equality branch only x != <immediate> remains a
+        ;; sound unary fact.  x != y with two non-immediates is
+        ;; relational and must not be encoded as a per-mvar constraint.
+        for skip = (and eq-fun negated (not op1-imm) (not op2-imm))
         for kind = (cl-case fun
                      (equal 'and-nhc)
                      (eql 'and-nhc)
                      (eq 'and)
                      (t fun))
-        when (or (comp--mvar-used-p target-mvar1)
-                 (comp--mvar-used-p target-mvar2))
+        when (and (not skip)
+                  (or (comp--mvar-used-p target-mvar1)
+                      (comp--mvar-used-p target-mvar2)))
         do
         (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
-                              (comp--maybe-add-vmvar op2 cmp-res prev-insns-seq)
+                              (if (comp-mvar-p op2)
+                                  (comp--maybe-add-vmvar op2 cmp-res prev-insns-seq)
+                                op2)
                               block-target negated))
           (when (comp--mvar-used-p target-mvar2)
             (comp--emit-assume (comp--reverse-arithm-fun kind)
                               target-mvar2
-                              (comp--maybe-add-vmvar op1 cmp-res prev-insns-seq)
+                              (if (comp-mvar-p op1)
+                                  (comp--maybe-add-vmvar op1 cmp-res prev-insns-seq)
+                                op1)
                               block-target negated)))
         finally (cl-return-from in-the-basic-block)))
       (`((set ,(and (pred comp-mvar-p) cmp-res)
diff --git a/test/src/comp-resources/comp-test-funcs.el b/test/src/comp-resources/comp-test-funcs.el
index 200d3f6793d..80baf503b11 100644
--- a/test/src/comp-resources/comp-test-funcs.el
+++ b/test/src/comp-resources/comp-test-funcs.el
@@ -590,6 +590,20 @@
            1
          x)))
 
+(defvar comp-test-80327-hash
+  (let ((h (make-hash-table :test #'eq)))
+    (puthash 321 4 h)
+    h))
+
+(defun comp-test-80327-f ()
+  (let* ((a (gethash 321 comp-test-80327-hash))
+         (b (logior a 2)))
+    (setq b (logior b 1))
+    (if (and (equal b a)
+             (not (equal b 0)))
+        1234
+      b)))
+
 
 ;;;;;;;;;;;;;;;;;;;;
 ;; Tromey's tests ;;
diff --git a/test/src/comp-tests.el b/test/src/comp-tests.el
index 28418cc9b86..fad71c282af 100644
--- a/test/src/comp-tests.el
+++ b/test/src/comp-tests.el
@@ -468,6 +468,10 @@ https://lists.gnu.org/archive/html/bug-gnu-emacs/2020-03/msg00914.html."
   "<https://lists.gnu.org/archive/html/bug-gnu-emacs/2020-12/msg01883.html>"
   (should (equal (comp-test-45376-2-f) '(0 2 1 0 1 0 1 0 0 0 0 0))))
 
+(comp-deftest bug-80327 ()
+  "Equal on a negated branch must not over-constrain operands."
+  (should (= (comp-test-80327-f) 7)))
+
 (defvar comp-test-primitive-advice)
 (comp-deftest primitive-advice ()
   "Test effectiveness of primitive advising."