[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
feature/native-comp c4efb49 3/5: Constrain mvars under compare and branc
From: |
Andrea Corallo |
Subject: |
feature/native-comp c4efb49 3/5: Constrain mvars under compare and branch with built-in predicates |
Date: |
Tue, 29 Dec 2020 11:51:59 -0500 (EST) |
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)) ()