mirror of
git://git.sv.gnu.org/emacs.git
synced 2025-12-15 10:30:25 -08:00
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.
This commit is contained in:
parent
715cac119a
commit
538f59806c
2 changed files with 23 additions and 6 deletions
|
|
@ -1891,6 +1891,7 @@ The assume is emitted at the beginning of the block BB."
|
||||||
(tmp-mvar (if negated
|
(tmp-mvar (if negated
|
||||||
(make-comp-mvar :slot (comp-mvar-slot rhs))
|
(make-comp-mvar :slot (comp-mvar-slot rhs))
|
||||||
rhs)))
|
rhs)))
|
||||||
|
(cl-assert lhs-slot)
|
||||||
(push `(assume ,(make-comp-mvar :slot lhs-slot) (and ,lhs ,tmp-mvar))
|
(push `(assume ,(make-comp-mvar :slot lhs-slot) (and ,lhs ,tmp-mvar))
|
||||||
(comp-block-insns bb))
|
(comp-block-insns bb))
|
||||||
(if negated
|
(if negated
|
||||||
|
|
@ -1898,7 +1899,7 @@ The assume is emitted at the beginning of the block BB."
|
||||||
(comp-block-insns bb)))
|
(comp-block-insns bb)))
|
||||||
(setf (comp-func-ssa-status comp-func) 'dirty)))
|
(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."
|
"Create a new basic-block named BB-SYMBOL and add it between BB-A and BB-B."
|
||||||
(cl-loop
|
(cl-loop
|
||||||
with new-bb = (make-comp-block-cstr :name bb-symbol
|
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)))
|
(comp-block-out-edges bb-a) (delq ed (comp-block-out-edges bb-a)))
|
||||||
(push ed (comp-block-out-edges new-bb))
|
(push ed (comp-block-out-edges new-bb))
|
||||||
;; Connect `bb-a' `new-bb' with `new-edge'.
|
;; Connect `bb-a' `new-bb' with `new-edge'.
|
||||||
(push (comp-block-out-edges bb-a) new-edge)
|
(push new-edge (comp-block-out-edges bb-a))
|
||||||
(push (comp-block-in-edges new-bb) new-edge)
|
(push new-edge (comp-block-in-edges new-bb))
|
||||||
(setf (comp-func-ssa-status comp-func) 'dirty)
|
(setf (comp-func-ssa-status comp-func) 'dirty)
|
||||||
;; Add `new-edge' to the current function and return it.
|
;; Add `new-edge' to the current function and return it.
|
||||||
(cl-return (puthash bb-symbol new-bb (comp-func-blocks comp-func)))
|
(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
|
;; If block has only one predecessor is already suitable for
|
||||||
;; adding constraint assumptions.
|
;; adding constraint assumptions.
|
||||||
target-bb
|
target-bb
|
||||||
(comp-add-new-block-beetween (intern (concat (symbol-name target-bb-sym)
|
(comp-add-new-block-between (intern (concat (symbol-name target-bb-sym)
|
||||||
"_cstrs"))
|
"_cstrs"))
|
||||||
curr-bb target-bb))))
|
curr-bb target-bb))))
|
||||||
|
|
||||||
(defun comp-add-cond-cstrs-simple ()
|
(defun comp-add-cond-cstrs-simple ()
|
||||||
"`comp-add-cstrs' worker function for each selected function."
|
"`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
|
do
|
||||||
(setf (car branch-target-cell) (comp-block-name block-target))
|
(setf (car branch-target-cell) (comp-block-name block-target))
|
||||||
(comp-emit-assume tmp-mvar obj2 block-target negated)
|
(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)))))))
|
finally (cl-return-from in-the-basic-block)))))))
|
||||||
|
|
||||||
(defun comp-add-cond-cstrs ()
|
(defun comp-add-cond-cstrs ()
|
||||||
|
|
|
||||||
|
|
@ -941,6 +941,12 @@ Return a list of results."
|
||||||
((defun comp-tests-ret-type-spec-f (x)
|
((defun comp-tests-ret-type-spec-f (x)
|
||||||
(when x
|
(when x
|
||||||
'foo))
|
'foo))
|
||||||
|
(or (member foo) null))
|
||||||
|
|
||||||
|
;; 21
|
||||||
|
((defun comp-tests-ret-type-spec-f (x)
|
||||||
|
(unless x
|
||||||
|
'foo))
|
||||||
(or (member foo) null))))
|
(or (member foo) null))))
|
||||||
|
|
||||||
(defun comp-tests-define-type-spec-test (number x)
|
(defun comp-tests-define-type-spec-test (number x)
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue