mirrors/emacs
1
Fork 0
mirror of git://git.sv.gnu.org/emacs.git synced 2025-12-15 10:30:25 -08:00
Code Issues Projects Releases Wiki Activity

Don't treat '=' as simple equality emitting constraints (bug#46812)

Browse source 
Extend assumes allowing the following form

(assume dst (= src1 src2))

to caputure '=' semanting during fwprop handling float integer
conversions.

	* lisp/emacs-lisp/comp.el (comp-equality-fun-p): Don't treat '=' as
	simple equality.
	(comp-arithm-cmp-fun-p, comp-negate-arithm-cmp-fun)
	(comp-reverse-arithm-fun): Rename and add '=' '!='.
	(comp-emit-assume, comp-add-cond-cstrs, comp-fwprop-insn): Update
	for new function nameing and to handle '='.
	* lisp/emacs-lisp/comp-cstr.el (comp-cstr-=): New function.
	* test/src/comp-tests.el (comp-tests-type-spec-tests): Add a bunch
	of '=' specific tests.
This commit is contained in:
Andrea Corallo 2021-02-27 22:00:11 +01:00
parent 2acc46b55b
commit 5bc08559e8
3 changed files with 75 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -859,6 +859,18 @@ Non memoized version of `comp-cstr-intersection-no-mem'."
(null (neg cstr))
(equal (typeset cstr) '(cons)))))
(defun comp-cstr-= (dst old-dst src)
"Constraint DST being = SRC."
(with-comp-cstr-accessors
(comp-cstr-intersection dst old-dst src)
(cl-loop for v in (valset dst)
when (and (floatp v)
(= v (truncate v)))
do (push (cons (truncate v) (truncate v)) (range dst)))
(cl-loop for (l . h) in (range dst)
when (eql l h)
do (push (float l) (valset dst)))))
(defun comp-cstr-> (dst old-dst src)
"Constraint DST being > than SRC.
SRC can be either a comp-cstr or an integer."

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

@ -906,11 +906,11 @@ To be used by all entry points."
(defun comp-equality-fun-p (function)
"Equality functions predicate for FUNCTION."
(when (memq function '(eq eql = equal)) t))
(when (memq function '(eq eql equal)) t))
(defun comp-range-cmp-fun-p (function)
"Predicate for range comparision functions."
(when (memq function '(> < >= <=)) t))
(defun comp-arithm-cmp-fun-p (function)
"Predicate for arithmetic comparision functions."
(when (memq function '(= > < >= <=)) t))
(defun comp-set-op-p (op)
"Assignment predicate for OP."
@ -2238,17 +2238,21 @@ into the C code forwarding the compilation unit."
else
do (comp-collect-mvars args))))
(defun comp-negate-range-cmp-fun (function)
"Negate FUNCTION."
(defun comp-negate-arithm-cmp-fun (function)
"Negate FUNCTION.
Return nil if we don't want to emit constraints for its
negation."
(cl-ecase function
(= nil)
(> '<=)
(< '>=)
(>= '<)
(<= '>)))
(defun comp-reverse-cmp-fun (function)
(defun comp-reverse-arithm-fun (function)
"Reverse FUNCTION."
(cl-case function
(= '=)
(> '<)
(< '>)
(>= '<=)
@ -2279,15 +2283,16 @@ The assume is emitted at the beginning of the block BB."
(comp-cstr-negation-make rhs)
rhs)))
(comp-block-insns bb))))
((pred comp-range-cmp-fun-p)
(let ((kind (if negated
(comp-negate-range-cmp-fun kind)
kind)))
((pred comp-arithm-cmp-fun-p)
(when-let ((kind (if negated
(comp-negate-arithm-cmp-fun kind)
kind)))
(push `(assume ,(make-comp-mvar :slot lhs-slot)
(,kind ,lhs
,(if-let* ((vld (comp-cstr-imm-vld-p rhs))
(val (comp-cstr-imm rhs))
(ok (integerp val)))
(ok (and (integerp val)
(not (memq kind '(= !=))))))
val
(make-comp-mvar :slot (comp-mvar-slot rhs)))))
(comp-block-insns bb))))
@ -2418,7 +2423,7 @@ TARGET-BB-SYM is the symbol name of the target block."
(`((set ,(and (pred comp-mvar-p) cmp-res)
(,(pred comp-call-op-p)
,(and (or (pred comp-equality-fun-p)
(pred comp-range-cmp-fun-p))
(pred comp-arithm-cmp-fun-p))
fun)
,op1 ,op2))
;; (comment ,_comment-str)
@ -2441,7 +2446,7 @@ TARGET-BB-SYM is the symbol name of the target block."
(comp-maybe-add-vmvar op2 cmp-res prev-insns-seq)
block-target negated))
(when (comp-mvar-used-p target-mvar2)
(comp-emit-assume (comp-reverse-cmp-fun kind)
(comp-emit-assume (comp-reverse-arithm-fun kind)
target-mvar2
(comp-maybe-add-vmvar op1 cmp-res prev-insns-seq)
block-target negated)))
@ -3108,7 +3113,9 @@ Fold the call in case."
(<
(comp-cstr-< lval (car operands) (cadr operands)))
(<=
(comp-cstr-<= lval (car operands) (cadr operands)))))
(comp-cstr-<= lval (car operands) (cadr operands)))
(=
(comp-cstr-= lval (car operands) (cadr operands)))))
(`(setimm ,lval ,v)
(setf (comp-cstr-imm lval) v))
(`(phi ,lval . ,rest)

47
test/src/comp-tests.el
View file

@ -891,24 +891,24 @@ Return a list of results."
;; 10
((defun comp-tests-ret-type-spec-f (x)
(if (= x 3)
(if (eql x 3)
x
'foo))
(or (member foo) (integer 3 3)))
;; 11
((defun comp-tests-ret-type-spec-f (x)
(if (= 3 x)
(if (eql 3 x)
x
'foo))
(or (member foo) (integer 3 3)))
;; 12
((defun comp-tests-ret-type-spec-f (x)
(if (= x 3)
(if (eql x 3)
'foo
x))
(or (member foo) marker number))
(not (integer 3 3)))
;; 13
((defun comp-tests-ret-type-spec-f (x y)
@ -1214,7 +1214,7 @@ Return a list of results."
;; 57
((defun comp-tests-ret-type-spec-f (x)
(unless (or (eq x 'foo)
(= x 3))
(eql x 3))
(error "Not foo or 3"))
x)
(or (member foo) (integer 3 3)))
@ -1244,7 +1244,42 @@ Return a list of results."
(>= x y))
x
(error "")))
(or float (integer 3 10)))))
(or float (integer 3 10)))
;; 61
((defun comp-tests-ret-type-spec-f (x)
(if (= x 1.0)
x
(error "")))
(or (member 1.0) (integer 1 1)))
;; 62
((defun comp-tests-ret-type-spec-f (x)
(if (= x 1.0)
x
(error "")))
(or (member 1.0) (integer 1 1)))
;; 63
((defun comp-tests-ret-type-spec-f (x)
(if (= x 1.1)
x
(error "")))
(member 1.1))
;; 64
((defun comp-tests-ret-type-spec-f (x)
(if (= x 1)
x
(error "")))
(or (member 1.0) (integer 1 1)))
;; 65
((defun comp-tests-ret-type-spec-f (x)
(if (= x 1)
x
(error "")))
(or (member 1.0) (integer 1 1)))))
(defun comp-tests-define-type-spec-test (number x)
`(comp-deftest ,(intern (format "ret-type-spec-%d" number)) ()