		Search-engine friendly clone of the ACL2 documentation.

Arith-compare-check

Vl-expr-arith-compare-warn

Signature
(vl-expr-arith-compare-warn x ss) → warnings
Arguments: x — Guard (vl-expr-p x).; ss — Guard (vl-scopestack-p ss).
Returns: warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-expr-arith-compare-warn

(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: vl-warninglist-p-of-vl-expr-arith-compare-warn

(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)