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.
This commit is contained in:
Andrea Corallo 2026-03-11 16:54:46 +01:00
parent d3adff8c8f
commit 40f4fc1d8c
3 changed files with 34 additions and 4 deletions

View file

@ -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)

View file

@ -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 ;;

View file

@ -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."