feature/native-comp c4efb49 3/5: Constrain mvars under compare and branch with built-in predicates

[Andrea Corallo]

branch: feature/native-comp
commit c4efb49a27f05284d28eac7f60b28495c68f63fb
Author: Andrea Corallo <akrl@sdf.org>
Commit: Andrea Corallo <akrl@sdf.org>

    Constrain mvars under compare and branch with built-in predicates
    
        * lisp/emacs-lisp/comp.el (comp-emit-assume): Update.
        (comp-known-predicate-p): New function.
        (comp-add-cond-cstrs): Extend to pattern match predicate calls.
        * lisp/emacs-lisp/comp-cstr.el (comp-cstr-null-p)
        (comp-pred-to-cstr): New function.
        * test/src/comp-tests.el (comp-tests-type-spec-tests): Add a
        number of tests and fix comments.
---
 lisp/emacs-lisp/comp-cstr.el | 11 +++++++
 lisp/emacs-lisp/comp.el      | 69 ++++++++++++++++++++++++++++++++++++++------
 test/src/comp-tests.el       | 69 +++++++++++++++++++++++++++++++++-----------
 3 files changed, 123 insertions(+), 26 deletions(-)

diff --git a/lisp/emacs-lisp/comp-cstr.el b/lisp/emacs-lisp/comp-cstr.el
index 8a8e22e..ce70242 100644
--- a/lisp/emacs-lisp/comp-cstr.el
+++ b/lisp/emacs-lisp/comp-cstr.el
@@ -137,6 +137,13 @@ Integer values are handled in the `range' slot.")
          (null (valset cstr))
          (null (range cstr)))))
 
+(defsubst comp-cstr-null-p (x)
+  "Return t if CSTR is equivalent to the `null' type specifier, nil otherwise."
+  (with-comp-cstr-accessors
+    (and (null (typeset x))
+         (null (range x))
+         (equal (valset x) '(nil)))))
+
 (defun comp-cstrs-homogeneous (cstrs)
   "Check if constraints CSTRS are all homogeneously negated or non-negated.
 Return `pos' if they are all positive, `neg' if they are all
@@ -167,6 +174,10 @@ Return them as multiple value."
                                       :range '((1 . 1)))
   "Represent the integer immediate one (1).")
 
+(defun comp-pred-to-cstr (predicate)
+  "Given PREDICATE return the correspondig constraint."
+  (comp-type-to-cstr (get predicate 'cl-satisfies-deftype)))
+
 
 ;;; Value handling.
 
diff --git a/lisp/emacs-lisp/comp.el b/lisp/emacs-lisp/comp.el
index 35a9e05..b885ff8 100644
--- a/lisp/emacs-lisp/comp.el
+++ b/lisp/emacs-lisp/comp.el
@@ -1895,7 +1895,10 @@ into the C code forwarding the compilation unit."
 ;;    in the CFG to infer information on the tested variables.
 ;;
 ;;  - Range propagation under test and branch (when the test is an
-;;    arithmetic comparison.)
+;;    arithmetic comparison).
+;;
+;;  - Type constraint under test and branch (when the test is a
+;;    known predicate).
 ;;
 ;;  - Function calls: function calls to function assumed to be not
 ;;    redefinable can be used to add constrains on the function
@@ -1956,15 +1959,22 @@ The assume is emitted at the beginning of the block BB."
     (cl-assert lhs-slot)
     (pcase kind
       ('and
-       (let ((tmp-mvar (if negated
-                          (make-comp-mvar :slot (comp-mvar-slot rhs))
-                        rhs)))
+       (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))
+                  (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 ,tmp-mvar))
-              (comp-block-insns bb))
-         (if negated
-             (push `(assume ,tmp-mvar (not ,rhs))
-                  (comp-block-insns bb)))))
+                        (and ,lhs ,(if negated
+                                       (comp-cstr-negation-make rhs)
+                                     rhs)))
+              (comp-block-insns bb))))
       ((pred comp-range-cmp-fun-p)
        (let ((kind (if negated
                        (comp-negate-range-cmp-fun kind)
@@ -2078,6 +2088,10 @@ TARGET-BB-SYM is the symbol name of the target block."
           (comp-emit-assume 'and obj1 obj2 block-target negated))
         finally (cl-return-from in-the-basic-block)))))))
 
+(defun comp-known-predicate-p (pred)
+  (when (symbolp pred)
+    (get pred 'cl-satisfies-deftype)))
+
 (defun comp-add-cond-cstrs ()
   "`comp-add-cstrs' worker function for each selected function."
   (cl-loop
@@ -2114,6 +2128,43 @@ TARGET-BB-SYM is the symbol name of the target block."
           (when (comp-mvar-used-p target-mvar2)
             (comp-emit-assume (comp-reverse-cmp-fun kind)
                               target-mvar2 op1 block-target negated)))
+        finally (cl-return-from in-the-basic-block)))
+      (`((set ,(and (pred comp-mvar-p) cmp-res)
+              (,(pred comp-call-op-p)
+               ,(and (pred comp-known-predicate-p) fun)
+               ,op))
+        ;; (comment ,_comment-str)
+        (cond-jump ,cmp-res ,(pred comp-mvar-p) . ,blocks))
+       (cl-loop
+        with target-mvar = (comp-cond-cstrs-target-mvar op (car insns-seq) b)
+        with cstr = (comp-pred-to-cstr fun)
+        for branch-target-cell on blocks
+        for branch-target = (car branch-target-cell)
+        for negated in '(t nil)
+        when (comp-mvar-used-p target-mvar)
+        do
+        (let ((block-target (comp-add-cond-cstrs-target-block b 
branch-target)))
+          (setf (car branch-target-cell) (comp-block-name block-target))
+          (comp-emit-assume 'and target-mvar cstr block-target negated))
+        finally (cl-return-from in-the-basic-block)))
+      ;; Match predicate on the negated branch (unless).
+      (`((set ,(and (pred comp-mvar-p) cmp-res)
+              (,(pred comp-call-op-p)
+               ,(and (pred comp-known-predicate-p) fun)
+               ,op))
+         (set ,neg-cmp-res (call eq ,cmp-res ,(pred comp-cstr-null-p)))
+        (cond-jump ,neg-cmp-res ,(pred comp-mvar-p) . ,blocks))
+       (cl-loop
+        with target-mvar = (comp-cond-cstrs-target-mvar op (car insns-seq) b)
+        with cstr = (comp-pred-to-cstr fun)
+        for branch-target-cell on blocks
+        for branch-target = (car branch-target-cell)
+        for negated in '(nil t)
+        when (comp-mvar-used-p target-mvar)
+        do
+        (let ((block-target (comp-add-cond-cstrs-target-block b 
branch-target)))
+          (setf (car branch-target-cell) (comp-block-name block-target))
+          (comp-emit-assume 'and target-mvar cstr block-target negated))
         finally (cl-return-from in-the-basic-block)))))))
 
 (defun comp-emit-call-cstr (mvar call-cell cstr)
diff --git a/test/src/comp-tests.el b/test/src/comp-tests.el
index c79190e..240af10 100644
--- a/test/src/comp-tests.el
+++ b/test/src/comp-tests.el
@@ -837,7 +837,6 @@ Return a list of results."
            y))
        (or (integer 1 1) (integer 3 3)))
 
-
       ;; 6
       ((defun comp-tests-ret-type-spec-f (x)
          (if x
@@ -1035,8 +1034,6 @@ Return a list of results."
        (or null marker number))
 
       ;; 36
-      ;; SBCL: (OR (RATIONAL (5)) (SINGLE-FLOAT 5.0)
-      ;;           (DOUBLE-FLOAT 5.0d0) NULL) !?
       ((defun comp-tests-ret-type-spec-f (x y)
          (when (and (> x 3)
                     (> y 2))
@@ -1051,15 +1048,14 @@ Return a list of results."
            (+ x y)))
        (or null float (integer * 5)))
 
-      ;; 38 SBCL gives: (OR (RATIONAL (2) (10)) (SINGLE-FLOAT 2.0 10.0)
-      ;;                    (DOUBLE-FLOAT 2.0d0 10.0d0) NULL)!?
+      ;; 38
       ((defun comp-tests-ret-type-spec-f (x y)
          (when (and (< 1 x 5)
                    (< 1 y 5))
            (+ x y)))
        (or null float (integer 4 8)))
 
-      ;; 37
+      ;; 39
       ;; SBCL gives: (OR REAL NULL)
       ((defun comp-tests-ret-type-spec-f (x y)
                    (when (and (<= 1 x 10)
@@ -1067,7 +1063,7 @@ Return a list of results."
                      (+ x y)))
        (or null float (integer 3 13)))
 
-      ;; 38
+      ;; 40
       ;; SBCL: (OR REAL NULL)
       ((defun comp-tests-ret-type-spec-f (x y)
                    (when (and (<= 1 x 10)
@@ -1075,42 +1071,42 @@ Return a list of results."
                      (- x y)))
        (or null float (integer -2 8)))
 
-      ;; 39
+      ;; 41
       ((defun comp-tests-ret-type-spec-f (x y)
          (when (and (<= 1 x)
                     (<= 2 y 3))
            (- x y)))
        (or null float (integer -2 *)))
 
-      ;; 40
+      ;; 42
       ((defun comp-tests-ret-type-spec-f (x y)
          (when (and (<= 1 x 10)
                     (<= 2 y))
            (- x y)))
        (or null float (integer * 8)))
 
-      ;; 41
+      ;; 43
       ((defun comp-tests-ret-type-spec-f (x y)
                    (when (and (<= x 10)
                               (<= 2 y))
                      (- x y)))
        (or null float (integer * 8)))
 
-      ;; 42
+      ;; 44
       ((defun comp-tests-ret-type-spec-f (x y)
           (when (and (<= x 10)
                      (<= y 3))
             (- x y)))
        (or null float integer))
 
-      ;; 43
+      ;; 45
       ((defun comp-tests-ret-type-spec-f (x y)
           (when (and (<= 2 x)
                      (<= 3 y))
             (- x y)))
        (or null float integer))
 
-      ;; 44
+      ;; 46
       ;; SBCL: (OR (RATIONAL (6) (30)) (SINGLE-FLOAT 6.0 30.0)
       ;;           (DOUBLE-FLOAT 6.0d0 30.0d0) NULL)
       ((defun comp-tests-ret-type-spec-f (x y z i j k)
@@ -1123,22 +1119,61 @@ Return a list of results."
            (+ x y z i j k)))
        (or null float (integer 12 24)))
 
-      ;; 45
+      ;; 47
       ((defun comp-tests-ret-type-spec-f (x)
          (when (<= 1 x 5)
            (1+ x)))
        (or null float (integer 2 6)))
 
-      ;;46
+      ;;48
       ((defun comp-tests-ret-type-spec-f (x)
          (when (<= 1 x 5)
            (1- x)))
        (or null float (integer 0 4)))
 
-      ;; 47
+      ;; 49
       ((defun comp-tests-ret-type-spec-f ()
          (error "foo"))
-       nil)))
+       nil)
+
+      ;; 50
+      ((defun comp-tests-ret-type-spec-f (x)
+         (if (stringp x)
+            x
+           'bar))
+       (or (member bar) string))
+
+      ;; 51
+      ((defun comp-tests-ret-type-spec-f (x)
+         (if (stringp x)
+             'bar
+           x))
+       (not string))
+
+      ;; 52
+      ((defun comp-tests-ret-type-spec-f (x)
+         (if (integerp x)
+             x
+           'bar))
+       (or (member bar) integer))
+
+      ;; 53
+      ((defun comp-tests-ret-type-spec-f (x)
+         (when (integerp x)
+           x))
+       (or null integer))
+
+      ;; 54
+      ((defun comp-tests-ret-type-spec-f (x)
+         (unless (symbolp x)
+           x))
+       (not symbol))
+
+      ;; 55
+      ((defun comp-tests-ret-type-spec-f (x)
+         (unless (integerp x)
+           x))
+       (not integer))))
 
   (defun comp-tests-define-type-spec-test (number x)
     `(comp-deftest ,(intern (format "ret-type-spec-%d" number)) ()