(vl-expr-arith-compare-warn x ss) → warnings
Function:
(defun vl-expr-arith-compare-warn (x ss) (declare (xargs :guard (and (vl-expr-p x) (vl-scopestack-p ss)))) (let ((__function__ 'vl-expr-arith-compare-warn)) (declare (ignorable __function__)) (b* ((x (vl-expr-fix x)) (warnings nil)) (vl-expr-case x :vl-binary (and (member x.op '(:vl-binary-eq :vl-binary-neq :vl-binary-lt :vl-binary-lte :vl-binary-gt :vl-binary-gte :vl-binary-ceq :vl-binary-cne :vl-binary-wildeq :vl-binary-wildneq)) (or (vl-expr-is-arith x.left) (vl-expr-is-arith x.right)) (b* ((scopes (vl-elabscopes-init-ss ss)) ((mv ?warns left-size) (vl-expr-selfsize x.left ss scopes)) ((mv ?warns right-size) (vl-expr-selfsize x.right ss scopes)) ((mv ?warns left-class) (vl-expr-typedecide x.left ss scopes)) ((mv ?warns right-class) (vl-expr-typedecide x.right ss scopes)) ((unless (and left-size right-size (vl-integer-arithclass-p left-class) (vl-integer-arithclass-p right-class))) nil) (size (max left-size right-size)) (type (vl-integer-arithclass->exprsign (vl-arithclass-max left-class right-class))) ((mv left-ok left-min left-max) (vl-arith-expr-range x.left size type ss scopes)) ((mv right-ok right-min right-max) (vl-arith-expr-range x.right size type ss scopes)) ((mv ?ok size-min size-max) (vl-arith-range-from-size/type size type)) ((unless (and left-ok right-ok)) nil) ((mv left-warning left-severity) (if (vl-expr-is-arith x.left) (cond ((> left-max size-max) (mv t t)) ((< left-min size-min) (mv t nil)) (t (mv nil nil))) (mv nil nil))) ((mv right-warning right-severity) (if (vl-expr-is-arith x.right) (cond ((> right-max size-max) (mv t t)) ((< right-min size-min) (mv t nil)) (t (mv nil nil))) (mv nil nil))) ((unless (or left-warning right-warning)) nil) (severity (or (and left-warning left-severity) (and right-warning right-severity))) (left-msg (and left-warning (vmsg "the value range of the left-hand-side may ~ ~s0~s1 that." (if (> left-max size-max) "overflow" "underflow") (if (and (> left-max size-max) (< left-min size-min)) " or underflow" "")))) (right-msg (and right-warning (vmsg "the value range of the right-hand-side may ~ ~s0~s1 that." (if (> right-max size-max) "overflow" "underflow") (if (and (> right-max size-max) (< right-min size-min)) " or underflow" "")))) (first-msg (or left-msg right-msg)) (second-msg (if (and left-msg right-msg) (vmsg " Additionally, ~@0" right-msg) ""))) (warn :type (if severity :vl-warn-arithmetic-comparison :vl-warn-arithmetic-comparison-minor) :msg "The comparison ~a0 involves an arithmetic expression ~ on ~s1. Such expressions are often not sized ~ according to reasonable expectations. The final ~ size of both sides is ~x2 (~s3), but ~@4~@5" :args (list x (if left-warning (if right-warning "both sides" "the left-hand side") "the right-hand side") size (if (eq (vl-exprsign-fix type) :vl-unsigned) "unsigned" "signed") first-msg second-msg)))) :otherwise nil))))
Theorem:
(defthm vl-warninglist-p-of-vl-expr-arith-compare-warn (b* ((warnings (vl-expr-arith-compare-warn x ss))) (vl-warninglist-p warnings)) :rule-classes :rewrite)