1
Fork 0
mirror of git://git.sv.gnu.org/emacs.git synced 2025-12-10 00:00:39 -08:00

comp: Propagate pre slot access type check

* lisp/loadup.el (max-lisp-eval-depth): Increase
`max-lisp-eval-depth' to 3400.

* lisp/emacs-lisp/comp.el (comp-add-cond-cstrs): Pattern match pre
slot access type check and add constraint.

* lisp/emacs-lisp/comp-cstr.el (comp-cstr-cl-tag-p)
(comp-cstr-cl-tag): New functions.

* lisp/emacs-lisp/comp.el (make-comp-mvar): Add neg parameter.
This commit is contained in:
Andrea Corallo 2023-05-17 18:00:24 +02:00
parent d03dd07774
commit 6c781b5d25
3 changed files with 34 additions and 2 deletions

View file

@ -895,6 +895,23 @@ Non memoized version of `comp-cstr-intersection-no-mem'."
(null (neg cstr))
(equal (typeset cstr) '(cons)))))
;; Move to comp.el?
(defsubst comp-cstr-cl-tag-p (cstr)
"Return non-nil if CSTR is a CL tag."
(with-comp-cstr-accessors
(and (null (range cstr))
(null (neg cstr))
(null (typeset cstr))
(length= (valset cstr) 1)
(string-match (rx "cl-struct-" (group-n 1 (1+ not-newline)) "-tags")
(symbol-name (car (valset cstr)))))))
(defsubst comp-cstr-cl-tag (cstr)
"If CSTR is a CL tag return its tag name."
(with-comp-cstr-accessors
(and (comp-cstr-cl-tag-p cstr)
(intern (match-string 1 (symbol-name (car (valset cstr))))))))
(defun comp-cstr-= (dst op1 op2)
"Constraint OP1 being = OP2 setting the result into DST."
(with-comp-cstr-accessors

View file

@ -1543,7 +1543,7 @@ STACK-OFF is the index of the first slot frame involved."
for sp from stack-off
collect (comp-slot-n sp))))
(cl-defun make-comp-mvar (&key slot (constant nil const-vld) type)
(cl-defun make-comp-mvar (&key slot (constant nil const-vld) type neg)
"`comp-mvar' initializer."
(let ((mvar (make--comp-mvar :slot slot)))
(when const-vld
@ -1551,6 +1551,8 @@ STACK-OFF is the index of the first slot frame involved."
(setf (comp-cstr-imm mvar) constant))
(when type
(setf (comp-mvar-typeset mvar) (list type)))
(when neg
(setf (comp-mvar-neg mvar) t))
mvar))
(defun comp-new-frame (size vsize &optional ssa)
@ -2546,6 +2548,19 @@ TARGET-BB-SYM is the symbol name of the target block."
for insns-seq on (comp-block-insns b)
do
(pcase insns-seq
(`((set ,(and (pred comp-mvar-p) mvar-tested-copy)
,(and (pred comp-mvar-p) mvar-tested))
(set ,(and (pred comp-mvar-p) mvar-1)
(call type-of ,(and (pred comp-mvar-p) mvar-tested-copy)))
(set ,(and (pred comp-mvar-p) mvar-2)
(call symbol-value ,(and (pred comp-cstr-cl-tag-p) mvar-tag)))
(set ,(and (pred comp-mvar-p) mvar-3)
(call memq ,(and (pred comp-mvar-p) mvar-1) ,(and (pred comp-mvar-p) mvar-2)))
(cond-jump ,(and (pred comp-mvar-p) mvar-3) ,(pred comp-mvar-p) ,bb1 ,bb2))
(push `(assume ,mvar-tested ,(make-comp-mvar :type (comp-cstr-cl-tag mvar-tag)))
(comp-block-insns (comp-add-cond-cstrs-target-block b bb2)))
(push `(assume ,mvar-tested ,(make-comp-mvar :type (comp-cstr-cl-tag mvar-tag) :neg t))
(comp-block-insns (comp-add-cond-cstrs-target-block b bb1))))
(`((set ,(and (pred comp-mvar-p) cmp-res)
(,(pred comp-call-op-p)
,(and (or (pred comp-equality-fun-p)