From 3d014e1bf48f661f0b229ddf735608ff0ba7cfe6 Mon Sep 17 00:00:00 2001
From: Andrea Corallo <akrl@sdf.org>
Date: Mon, 1 Mar 2021 19:39:00 +0100
Subject: Fix `eql' `equal' propagation of non hash consed values (bug#46843)

Extend assumes allowing the following form:

(assume dst (and-nhc src1 src2))

`and-nhc' assume operator allow for constraining correctly
intersections where non hash consed values are not propagated as
values but rather promoted to their types.

	* lisp/emacs-lisp/comp-cstr.el
	(comp-cstr-intersection-no-hashcons): New function.
	* lisp/emacs-lisp/comp.el (comp-emit-assume): Logic update to emit
	`and-nhc' operator (implemented in fwprop by
	`comp-cstr-intersection-no-hashcons').
	(comp-add-cond-cstrs): Map `eq' to `and' assume operator and
	`equal' `eql' into `and-nhc'.
	(comp-fwprop-insn): Update to handle `and-nhc'.
	* test/src/comp-tests.el (comp-tests-type-spec-tests): Add two
	tests covering `eql' and `equal' propagation of non hash consed
	values.
---
 lisp/emacs-lisp/comp.el | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

(limited to 'lisp/emacs-lisp/comp.el')

diff --git a/lisp/emacs-lisp/comp.el b/lisp/emacs-lisp/comp.el
index 03999d3e66f..af14afd42bb 100644
--- a/lisp/emacs-lisp/comp.el
+++ b/lisp/emacs-lisp/comp.el
@@ -2266,20 +2266,20 @@ The assume is emitted at the beginning of the block BB."
   (let ((lhs-slot (comp-mvar-slot lhs)))
     (cl-assert lhs-slot)
     (pcase kind
-      ('and
+      ((or 'and 'and-nhc)
        (if (comp-mvar-p rhs)
            (let ((tmp-mvar (if negated
                                (make-comp-mvar :slot (comp-mvar-slot rhs))
                              rhs)))
              (push `(assume ,(make-comp-mvar :slot lhs-slot)
-                            (and ,lhs ,tmp-mvar))
+                            (,kind ,lhs ,tmp-mvar))
 	           (comp-block-insns bb))
              (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
+                        (,kind ,lhs ,(if negated
                                        (comp-cstr-negation-make rhs)
                                      rhs)))
 	       (comp-block-insns bb))))
@@ -2431,11 +2431,14 @@ TARGET-BB-SYM is the symbol name of the target block."
        (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 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)
+        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))
         do
@@ -3102,6 +3105,8 @@ Fold the call in case."
      (cl-case kind
        (and
         (apply #'comp-cstr-intersection lval operands))
+       (and-nhc
+        (apply #'comp-cstr-intersection-no-hashcons lval operands))
        (not
         ;; Prevent double negation!
         (unless (comp-cstr-neg (car operands))
-- 
cgit v1.2.3