diff options
| author | Andrea Corallo | 2021-03-01 19:39:00 +0100 |
|---|---|---|
| committer | Andrea Corallo | 2021-03-01 18:09:40 +0100 |
| commit | 3d014e1bf48f661f0b229ddf735608ff0ba7cfe6 (patch) | |
| tree | 43546114820b1146cd0bc37c015ccd8a9a1dfed5 | |
| parent | 5bc08559e8f171eafc3c034232f8cfd9eaf89862 (diff) | |
| download | emacs-3d014e1bf48f661f0b229ddf735608ff0ba7cfe6.tar.gz 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.
| -rw-r--r-- | lisp/emacs-lisp/comp-cstr.el | 22 | ||||
| -rw-r--r-- | lisp/emacs-lisp/comp.el | 15 | ||||
| -rw-r--r-- | 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 bd1e04fb0bb..d98ef681b58 100644 --- a/lisp/emacs-lisp/comp-cstr.el +++ b/lisp/emacs-lisp/comp-cstr.el | |||
| @@ -968,6 +968,28 @@ DST is returned." | |||
| 968 | (neg dst) (neg res)) | 968 | (neg dst) (neg res)) |
| 969 | res))) | 969 | res))) |
| 970 | 970 | ||
| 971 | (defun comp-cstr-intersection-no-hashcons (dst &rest srcs) | ||
| 972 | "Combine SRCS by intersection set operation setting the result in DST. | ||
| 973 | Non hash consed values are not propagated as values but rather | ||
| 974 | promoted to their types. | ||
| 975 | DST is returned." | ||
| 976 | (with-comp-cstr-accessors | ||
| 977 | (apply #'comp-cstr-intersection dst srcs) | ||
| 978 | (let (strip-values strip-types) | ||
| 979 | (cl-loop for v in (valset dst) | ||
| 980 | unless (or (symbolp v) | ||
| 981 | (fixnump v)) | ||
| 982 | do (push v strip-values) | ||
| 983 | (push (type-of v) strip-types)) | ||
| 984 | (when strip-values | ||
| 985 | (setf (typeset dst) (comp-union-typesets (typeset dst) strip-types) | ||
| 986 | (valset dst) (cl-set-difference (valset dst) strip-values))) | ||
| 987 | (cl-loop for (l . h) in (range dst) | ||
| 988 | when (or (bignump l) (bignump h)) | ||
| 989 | do (setf (range dst) '((- . +))) | ||
| 990 | (cl-return)) | ||
| 991 | dst))) | ||
| 992 | |||
| 971 | (defun comp-cstr-intersection-make (&rest srcs) | 993 | (defun comp-cstr-intersection-make (&rest srcs) |
| 972 | "Combine SRCS by intersection set operation and return a new constraint." | 994 | "Combine SRCS by intersection set operation and return a new constraint." |
| 973 | (apply #'comp-cstr-intersection (make-comp-cstr) srcs)) | 995 | (apply #'comp-cstr-intersection (make-comp-cstr) srcs)) |
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." | |||
| 2266 | (let ((lhs-slot (comp-mvar-slot lhs))) | 2266 | (let ((lhs-slot (comp-mvar-slot lhs))) |
| 2267 | (cl-assert lhs-slot) | 2267 | (cl-assert lhs-slot) |
| 2268 | (pcase kind | 2268 | (pcase kind |
| 2269 | ('and | 2269 | ((or 'and 'and-nhc) |
| 2270 | (if (comp-mvar-p rhs) | 2270 | (if (comp-mvar-p rhs) |
| 2271 | (let ((tmp-mvar (if negated | 2271 | (let ((tmp-mvar (if negated |
| 2272 | (make-comp-mvar :slot (comp-mvar-slot rhs)) | 2272 | (make-comp-mvar :slot (comp-mvar-slot rhs)) |
| 2273 | rhs))) | 2273 | rhs))) |
| 2274 | (push `(assume ,(make-comp-mvar :slot lhs-slot) | 2274 | (push `(assume ,(make-comp-mvar :slot lhs-slot) |
| 2275 | (and ,lhs ,tmp-mvar)) | 2275 | (,kind ,lhs ,tmp-mvar)) |
| 2276 | (comp-block-insns bb)) | 2276 | (comp-block-insns bb)) |
| 2277 | (if negated | 2277 | (if negated |
| 2278 | (push `(assume ,tmp-mvar (not ,rhs)) | 2278 | (push `(assume ,tmp-mvar (not ,rhs)) |
| 2279 | (comp-block-insns bb)))) | 2279 | (comp-block-insns bb)))) |
| 2280 | ;; If is only a constraint we can negate it directly. | 2280 | ;; If is only a constraint we can negate it directly. |
| 2281 | (push `(assume ,(make-comp-mvar :slot lhs-slot) | 2281 | (push `(assume ,(make-comp-mvar :slot lhs-slot) |
| 2282 | (and ,lhs ,(if negated | 2282 | (,kind ,lhs ,(if negated |
| 2283 | (comp-cstr-negation-make rhs) | 2283 | (comp-cstr-negation-make rhs) |
| 2284 | rhs))) | 2284 | rhs))) |
| 2285 | (comp-block-insns bb)))) | 2285 | (comp-block-insns bb)))) |
| @@ -2431,11 +2431,14 @@ TARGET-BB-SYM is the symbol name of the target block." | |||
| 2431 | (cl-loop | 2431 | (cl-loop |
| 2432 | with target-mvar1 = (comp-cond-cstrs-target-mvar op1 (car insns-seq) b) | 2432 | with target-mvar1 = (comp-cond-cstrs-target-mvar op1 (car insns-seq) b) |
| 2433 | with target-mvar2 = (comp-cond-cstrs-target-mvar op2 (car insns-seq) b) | 2433 | with target-mvar2 = (comp-cond-cstrs-target-mvar op2 (car insns-seq) b) |
| 2434 | with equality = (comp-equality-fun-p fun) | ||
| 2435 | for branch-target-cell on blocks | 2434 | for branch-target-cell on blocks |
| 2436 | for branch-target = (car branch-target-cell) | 2435 | for branch-target = (car branch-target-cell) |
| 2437 | for negated in '(t nil) | 2436 | for negated in '(t nil) |
| 2438 | for kind = (if equality 'and fun) | 2437 | for kind = (cl-case fun |
| 2438 | (equal 'and-nhc) | ||
| 2439 | (eql 'and-nhc) | ||
| 2440 | (eq 'and) | ||
| 2441 | (t fun)) | ||
| 2439 | when (or (comp-mvar-used-p target-mvar1) | 2442 | when (or (comp-mvar-used-p target-mvar1) |
| 2440 | (comp-mvar-used-p target-mvar2)) | 2443 | (comp-mvar-used-p target-mvar2)) |
| 2441 | do | 2444 | do |
| @@ -3102,6 +3105,8 @@ Fold the call in case." | |||
| 3102 | (cl-case kind | 3105 | (cl-case kind |
| 3103 | (and | 3106 | (and |
| 3104 | (apply #'comp-cstr-intersection lval operands)) | 3107 | (apply #'comp-cstr-intersection lval operands)) |
| 3108 | (and-nhc | ||
| 3109 | (apply #'comp-cstr-intersection-no-hashcons lval operands)) | ||
| 3105 | (not | 3110 | (not |
| 3106 | ;; Prevent double negation! | 3111 | ;; Prevent double negation! |
| 3107 | (unless (comp-cstr-neg (car operands)) | 3112 | (unless (comp-cstr-neg (car operands)) |
diff --git a/test/src/comp-tests.el b/test/src/comp-tests.el index 0598eeeb05d..651df332966 100644 --- a/test/src/comp-tests.el +++ b/test/src/comp-tests.el | |||
| @@ -1279,7 +1279,21 @@ Return a list of results." | |||
| 1279 | (if (= x 1) | 1279 | (if (= x 1) |
| 1280 | x | 1280 | x |
| 1281 | (error ""))) | 1281 | (error ""))) |
| 1282 | (or (member 1.0) (integer 1 1))))) | 1282 | (or (member 1.0) (integer 1 1))) |
| 1283 | |||
| 1284 | ;; 66 | ||
| 1285 | ((defun comp-tests-ret-type-spec-f (x) | ||
| 1286 | (if (eql x 0.0) | ||
| 1287 | x | ||
| 1288 | (error ""))) | ||
| 1289 | float) | ||
| 1290 | |||
| 1291 | ;; 67 | ||
| 1292 | ((defun comp-tests-ret-type-spec-f (x) | ||
| 1293 | (if (equal x '(1 2 3)) | ||
| 1294 | x | ||
| 1295 | (error ""))) | ||
| 1296 | cons))) | ||
| 1283 | 1297 | ||
| 1284 | (defun comp-tests-define-type-spec-test (number x) | 1298 | (defun comp-tests-define-type-spec-test (number x) |
| 1285 | `(comp-deftest ,(intern (format "ret-type-spec-%d" number)) () | 1299 | `(comp-deftest ,(intern (format "ret-type-spec-%d" number)) () |