Function: comp--emit-assume
comp--emit-assume is a byte-compiled function defined in comp.el.gz.
Signature
(comp--emit-assume KIND LHS RHS BB NEGATED)
Documentation
Emit an assume of kind KIND for mvar LHS being RHS.
When NEGATED is non-nil, the assumption is negated. The assume is emitted at the beginning of the block BB.
Source Code
;; Defined in /usr/src/emacs/lisp/emacs-lisp/comp.el.gz
(defun comp--emit-assume (kind lhs rhs bb negated)
"Emit an assume of kind KIND for mvar LHS being RHS.
When NEGATED is non-nil, the assumption is negated.
The assume is emitted at the beginning of the block BB."
(let ((lhs-slot (comp-mvar-slot lhs)))
(cl-assert lhs-slot)
(pcase kind
((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)
(,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)
(,kind ,lhs ,(if negated
(comp-cstr-negation-make rhs)
rhs)))
(comp-block-insns bb))))
((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 (and (integerp val)
(not (memq kind '(= !=))))))
val
(make--comp-mvar :slot (comp-mvar-slot rhs)))))
(comp-block-insns bb))))
(_ (cl-assert nil)))
(setf (comp-func-ssa-status comp-func) 'dirty)))