diff options
author | Andrea Corallo <akrl@sdf.org> | 2021-03-01 19:39:00 +0100 |
---|---|---|
committer | Andrea Corallo <akrl@sdf.org> | 2021-03-01 18:09:40 +0100 |
commit | 3d014e1bf48f661f0b229ddf735608ff0ba7cfe6 (patch) | |
tree | 43546114820b1146cd0bc37c015ccd8a9a1dfed5 /lisp/emacs-lisp/comp.el | |
parent | 5bc08559e8f171eafc3c034232f8cfd9eaf89862 (diff) | |
download | emacs-3d014e1bf48f661f0b229ddf735608ff0ba7cfe6.tar.gz emacs-3d014e1bf48f661f0b229ddf735608ff0ba7cfe6.tar.bz2 emacs-3d014e1bf48f661f0b229ddf735608ff0ba7cfe6.zip |
Fix `eql' `equal' propagation of non hash consed values (bug#46843)
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.
Diffstat (limited to 'lisp/emacs-lisp/comp.el')
-rw-r--r-- | lisp/emacs-lisp/comp.el | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/lisp/emacs-lisp/comp.el b/lisp/emacs-lisp/comp.el index 03999d3e66f..af14afd42bb 100644 --- a/lisp/emacs-lisp/comp.el +++ b/lisp/emacs-lisp/comp.el @@ -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)) |