Extend cstrs pass to match `unless' like code

	* lisp/emacs-lisp/comp.el (comp-emit-assume): Add assertion.
	(comp-add-new-block-between): Fix two typos.
	(comp-add-cond-cstrs-target-block): Fix typo.
	(comp-add-cond-cstrs-simple): Logic update.
	* test/src/comp-tests.el (comp-tests-type-spec-tests): Add a test.

diff --git a/lisp/emacs-lisp/comp.el b/lisp/emacs-lisp/comp.el
index ad09210d8dd644991a505521256fb5d72f395e0a..297dabbb5da695a605e88a7ebd018fc0b2549a86 100644 (file)
--- a/lisp/emacs-lisp/comp.el
+++ b/lisp/emacs-lisp/comp.el
@@ -1891,6 +1891,7 @@ The assume is emitted at the beginning of the block BB."
         (tmp-mvar (if negated
                       (make-comp-mvar :slot (comp-mvar-slot rhs))
                     rhs)))
+    (cl-assert lhs-slot)
     (push `(assume ,(make-comp-mvar :slot lhs-slot) (and ,lhs ,tmp-mvar))
          (comp-block-insns bb))
     (if negated
@@ -1898,7 +1899,7 @@ The assume is emitted at the beginning of the block BB."
              (comp-block-insns bb)))
     (setf (comp-func-ssa-status comp-func) 'dirty)))
 
-(defun comp-add-new-block-beetween (bb-symbol bb-a bb-b)
+(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."
   (cl-loop
    with new-bb = (make-comp-block-cstr :name bb-symbol
@@ -1913,8 +1914,8 @@ The assume is emitted at the beginning of the block BB."
          (comp-block-out-edges bb-a) (delq ed (comp-block-out-edges bb-a)))
    (push ed (comp-block-out-edges new-bb))
    ;; Connect `bb-a' `new-bb' with `new-edge'.
-   (push (comp-block-out-edges bb-a) new-edge)
-   (push (comp-block-in-edges new-bb) new-edge)
+   (push new-edge (comp-block-out-edges bb-a))
+   (push new-edge (comp-block-in-edges new-bb))
    (setf (comp-func-ssa-status comp-func) 'dirty)
    ;; Add `new-edge' to the current function and return it.
    (cl-return (puthash bb-symbol new-bb (comp-func-blocks comp-func)))
@@ -1948,9 +1949,9 @@ TARGET-BB-SYM is the symbol name of the target block."
         ;; If block has only one predecessor is already suitable for
         ;; adding constraint assumptions.
         target-bb
-      (comp-add-new-block-beetween (intern (concat (symbol-name target-bb-sym)
-                                                   "_cstrs"))
-                                   curr-bb target-bb))))
+      (comp-add-new-block-between (intern (concat (symbol-name target-bb-sym)
+                                                  "_cstrs"))
+                                  curr-bb target-bb))))
 
 (defun comp-add-cond-cstrs-simple ()
   "`comp-add-cstrs' worker function for each selected function."
@@ -1974,6 +1975,16 @@ TARGET-BB-SYM is the symbol name of the target block."
         do
         (setf (car branch-target-cell) (comp-block-name block-target))
         (comp-emit-assume tmp-mvar obj2 block-target negated)
+        finally (cl-return-from in-the-basic-block)))
+      (`((cond-jump ,obj1 ,obj2 . ,blocks))
+       (cl-loop
+        for branch-target-cell on blocks
+        for branch-target = (car branch-target-cell)
+        for block-target = (comp-add-cond-cstrs-target-block b branch-target)
+        for negated in '(nil t)
+        do
+        (setf (car branch-target-cell) (comp-block-name block-target))
+        (comp-emit-assume obj1 obj2 block-target negated)
         finally (cl-return-from in-the-basic-block)))))))
 
 (defun comp-add-cond-cstrs ()

diff --git a/test/src/comp-tests.el b/test/src/comp-tests.el
index 039e0665375503bba8d259f1b330397e81e0c75f..8f0b3406be64b88d08a73533097ae9ca913cea19 100644 (file)
--- a/test/src/comp-tests.el
+++ b/test/src/comp-tests.el
@@ -941,6 +941,12 @@ Return a list of results."
       ((defun comp-tests-ret-type-spec-f (x)
          (when x
            'foo))
+       (or (member foo) null))
+
+      ;; 21
+      ((defun comp-tests-ret-type-spec-f (x)
+         (unless x
+           'foo))
        (or (member foo) null))))
 
   (defun comp-tests-define-type-spec-test (number x)