From c4efb49a27f05284d28eac7f60b28495c68f63fb Mon Sep 17 00:00:00 2001 From: Andrea Corallo Date: Tue, 29 Dec 2020 13:29:02 +0100 Subject: [PATCH] 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 8a8e22e030d..ce702422932 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 35a9e05cfb7..b885ff88411 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 c79190e2967..240af102ec4 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)) () -- 2.39.5