aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAndrea Corallo2021-03-01 19:39:00 +0100
committerAndrea Corallo2021-03-01 18:09:40 +0100
commit3d014e1bf48f661f0b229ddf735608ff0ba7cfe6 (patch)
tree43546114820b1146cd0bc37c015ccd8a9a1dfed5
parent5bc08559e8f171eafc3c034232f8cfd9eaf89862 (diff)
downloademacs-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.el22
-rw-r--r--lisp/emacs-lisp/comp.el15
-rw-r--r--test/src/comp-tests.el16
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.
973Non hash consed values are not propagated as values but rather
974promoted to their types.
975DST 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)) ()