[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
feature/native-comp 3d014e1: Fix `eql' `equal' propagation of non hash c
From: |
Andrea Corallo |
Subject: |
feature/native-comp 3d014e1: Fix `eql' `equal' propagation of non hash consed values (bug#46843) |
Date: |
Mon, 1 Mar 2021 12:11:05 -0500 (EST) |
branch: feature/native-comp
commit 3d014e1bf48f661f0b229ddf735608ff0ba7cfe6
Author: Andrea Corallo <akrl@sdf.org>
Commit: Andrea Corallo <akrl@sdf.org>
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.
---
lisp/emacs-lisp/comp-cstr.el | 22 ++++++++++++++++++++++
lisp/emacs-lisp/comp.el | 15 ++++++++++-----
test/src/comp-tests.el | 16 +++++++++++++++-
3 files changed, 47 insertions(+), 6 deletions(-)
diff --git a/lisp/emacs-lisp/comp-cstr.el b/lisp/emacs-lisp/comp-cstr.el
index bd1e04f..d98ef68 100644
--- a/lisp/emacs-lisp/comp-cstr.el
+++ b/lisp/emacs-lisp/comp-cstr.el
@@ -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))
diff --git a/lisp/emacs-lisp/comp.el b/lisp/emacs-lisp/comp.el
index 03999d3..af14afd 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))
diff --git a/test/src/comp-tests.el b/test/src/comp-tests.el
index 0598eee..651df33 100644
--- a/test/src/comp-tests.el
+++ b/test/src/comp-tests.el
@@ -1279,7 +1279,21 @@ Return a list of results."
(if (= x 1)
x
(error "")))
- (or (member 1.0) (integer 1 1)))))
+ (or (member 1.0) (integer 1 1)))
+
+ ;; 66
+ ((defun comp-tests-ret-type-spec-f (x)
+ (if (eql x 0.0)
+ x
+ (error "")))
+ float)
+
+ ;; 67
+ ((defun comp-tests-ret-type-spec-f (x)
+ (if (equal x '(1 2 3))
+ x
+ (error "")))
+ cons)))
(defun comp-tests-define-type-spec-test (number x)
`(comp-deftest ,(intern (format "ret-type-spec-%d" number)) ()
[Prev in Thread] |
Current Thread |
[Next in Thread] |
- feature/native-comp 3d014e1: Fix `eql' `equal' propagation of non hash consed values (bug#46843),
Andrea Corallo <=