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.

diff --git a/lisp/emacs-lisp/comp-cstr.el b/lisp/emacs-lisp/comp-cstr.el
index bd1e04fb0bba1e1f19118dd5dc761d718e0dd91a..d98ef681b58df79add422e14183251350dba3129 100644 (file)
--- a/lisp/emacs-lisp/comp-cstr.el
+++ b/lisp/emacs-lisp/comp-cstr.el
@@ -968,6 +968,28 @@ DST is returned."
             (neg dst) (neg res))
       res)))
 
+(defun comp-cstr-intersection-no-hashcons (dst &rest srcs)
+  "Combine SRCS by intersection set operation setting the result in DST.
+Non hash consed values are not propagated as values but rather
+promoted to their types.
+DST is returned."
+  (with-comp-cstr-accessors
+    (apply #'comp-cstr-intersection dst srcs)
+    (let (strip-values strip-types)
+      (cl-loop for v in (valset dst)
+               unless (or (symbolp v)
+                          (fixnump v))
+                 do (push v strip-values)
+                    (push (type-of v) strip-types))
+      (when strip-values
+        (setf (typeset dst) (comp-union-typesets (typeset dst) strip-types)
+              (valset dst) (cl-set-difference (valset dst) strip-values)))
+      (cl-loop for (l . h) in (range dst)
+               when (or (bignump l) (bignump h))
+                 do (setf (range dst) '((- . +)))
+                    (cl-return))
+      dst)))
+
 (defun comp-cstr-intersection-make (&rest srcs)
   "Combine SRCS by intersection set operation and return a new constraint."
   (apply #'comp-cstr-intersection (make-comp-cstr) srcs))

diff --git a/lisp/emacs-lisp/comp.el b/lisp/emacs-lisp/comp.el
index 03999d3e66f834773a70adfc80b364111f38a8be..af14afd42bb1e03a5862478bc822c73dcbcff3c5 100644 (file)
--- 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))

diff --git a/test/src/comp-tests.el b/test/src/comp-tests.el
index 0598eeeb05dd45b46ad1e4e2fec43311f4fc1b8e..651df3329665fe68832e97524e9c8b532b730169 100644 (file)
--- a/test/src/comp-tests.el
+++ b/test/src/comp-tests.el
@@ -1279,7 +1279,21 @@ Return a list of results."
         (if (= x 1)
              x
            (error "")))
-       (or (member 1.0) (integer 1 1)))))
+       (or (member 1.0) (integer 1 1)))
+
+      ;; 66
+      ((defun comp-tests-ret-type-spec-f (x)
+        (if (eql x 0.0)
+            x
+          (error "")))
+       float)
+
+      ;; 67
+      ((defun comp-tests-ret-type-spec-f (x)
+        (if (equal x '(1 2 3))
+            x
+          (error "")))
+       cons)))
 
   (defun comp-tests-define-type-spec-test (number x)
     `(comp-deftest ,(intern (format "ret-type-spec-%d" number)) ()