From 538f59806c1994df7d77716f896db5602f59dc02 Mon Sep 17 00:00:00 2001 From: Andrea Corallo Date: Tue, 22 Dec 2020 15:00:44 +0100 Subject: [PATCH] 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. --- lisp/emacs-lisp/comp.el | 23 +++++++++++++++++------ test/src/comp-tests.el | 6 ++++++ 2 files changed, 23 insertions(+), 6 deletions(-) diff --git a/lisp/emacs-lisp/comp.el b/lisp/emacs-lisp/comp.el index ad09210d8dd..297dabbb5da 100644 --- 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 039e0665375..8f0b3406be6 100644 --- 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) -- 2.39.5