procyberian/emacs
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Fix eql' equal' propagation of non hash consed values (bug#46843)

Browse source 
Extend assumes allowing the following form:

(assume dst (and-nhc src1 src2))

`and-nhc' assume operator allow for constraining correctly
intersections where non hash consed values are not propagated as
values but rather promoted to their types.

	* lisp/emacs-lisp/comp-cstr.el
	(comp-cstr-intersection-no-hashcons): New function.
	* lisp/emacs-lisp/comp.el (comp-emit-assume): Logic update to emit
	`and-nhc' operator (implemented in fwprop by
	`comp-cstr-intersection-no-hashcons').
	(comp-add-cond-cstrs): Map `eq' to `and' assume operator and
	`equal' `eql' into `and-nhc'.
	(comp-fwprop-insn): Update to handle `and-nhc'.
	* test/src/comp-tests.el (comp-tests-type-spec-tests): Add two
	tests covering `eql' and `equal' propagation of non hash consed
	values.
This commit is contained in:
Andrea Corallo 2021-03-01 19:39:00 +01:00
parent 5bc08559e8
commit 3d014e1bf4
3 changed files with 47 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

22
lisp/emacs-lisp/comp-cstr.el
View file

@ -968,6 +968,28 @@ DST is returned."
(neg dst) (neg res))
res)))
(defun comp-cstr-intersection-no-hashcons (dst &rest srcs)
"Combine SRCS by intersection set operation setting the result in DST.
Non hash consed values are not propagated as values but rather
promoted to their types.
DST is returned."
(with-comp-cstr-accessors
(apply #'comp-cstr-intersection dst srcs)
(let (strip-values strip-types)
(cl-loop for v in (valset dst)
unless (or (symbolp v)
(fixnump v))
do (push v strip-values)
(push (type-of v) strip-types))
(when strip-values
(setf (typeset dst) (comp-union-typesets (typeset dst) strip-types)
(valset dst) (cl-set-difference (valset dst) strip-values)))
(cl-loop for (l . h) in (range dst)
when (or (bignump l) (bignump h))
do (setf (range dst) '((- . +)))
(cl-return))
dst)))
(defun comp-cstr-intersection-make (&rest srcs)
"Combine SRCS by intersection set operation and return a new constraint."
(apply #'comp-cstr-intersection (make-comp-cstr) srcs))

15
lisp/emacs-lisp/comp.el
View file

@ -2266,20 +2266,20 @@ The assume is emitted at the beginning of the block BB."
(let ((lhs-slot (comp-mvar-slot lhs)))
(cl-assert lhs-slot)
(pcase kind
('and
((or 'and 'and-nhc)
(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))
(,kind ,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 ,(if negated
(,kind ,lhs ,(if negated
(comp-cstr-negation-make rhs)
rhs)))
(comp-block-insns bb))))
@ -2431,11 +2431,14 @@ TARGET-BB-SYM is the symbol name of the target block."
(cl-loop
with target-mvar1 = (comp-cond-cstrs-target-mvar op1 (car insns-seq) b)
with target-mvar2 = (comp-cond-cstrs-target-mvar op2 (car insns-seq) b)
with equality = (comp-equality-fun-p fun)
for branch-target-cell on blocks
for branch-target = (car branch-target-cell)
for negated in '(t nil)
for kind = (if equality 'and fun)
for kind = (cl-case fun
(equal 'and-nhc)
(eql 'and-nhc)
(eq 'and)
(t fun))
when (or (comp-mvar-used-p target-mvar1)
(comp-mvar-used-p target-mvar2))
do
@ -3102,6 +3105,8 @@ Fold the call in case."
(cl-case kind
(and
(apply #'comp-cstr-intersection lval operands))
(and-nhc
(apply #'comp-cstr-intersection-no-hashcons lval operands))
(not
;; Prevent double negation!
(unless (comp-cstr-neg (car operands))