Heuristically categorize fussy warnings according to severity.
(vl-tweak-fussy-warning-type type a b asize bsize op) → adjusted-type
This function is called when we've just noticed that A and B have
different self-sizes but are used in an expression like
My original approach was just to say: the warning should be minor if ASIZE or BSIZE is 32. But this happens in many very common cases where unsized numbers are used, such as:
foo[3:0] == 7; // 4 bits == 32 bits foo[0] ? bar[3:0] : 0; // foo[0] ? 4 bits : 32 bits
Over time I have added many additional tweaks, see the comments for details.
Function:
(defun vl-tweak-fussy-warning-type (type a b asize bsize op) (declare (xargs :guard (and (symbolp type) (vl-expr-p a) (vl-expr-p b) (natp asize) (natp bsize) (vl-op-p op)))) (let ((__function__ 'vl-tweak-fussy-warning-type)) (declare (ignorable __function__)) (b* ((type (acl2::symbol-fix type)) (op (vl-op-fix op)) (asize (lnfix asize)) (bsize (lnfix bsize)) (a (vl-expr-fix a)) (b (vl-expr-fix b)) (a-zerop (and (vl-expr-resolved-p a) (eql (vl-resolved->val a) 0))) (b-zerop (and (vl-expr-resolved-p b) (eql (vl-resolved->val b) 0))) ((when (or a-zerop b-zerop)) nil) ((when (or (vl-expr-extint-p a) (vl-expr-extint-p b))) nil) (a-fits-b-p (and (vl-expr-resolved-p a) (unsigned-byte-p bsize (vl-resolved->val a)))) (b-fits-a-p (and (vl-expr-resolved-p b) (unsigned-byte-p asize (vl-resolved->val b)))) ((when (and (or a-fits-b-p b-fits-a-p) (member op '(:vl-binary-eq :vl-binary-neq :vl-binary-ceq :vl-binary-cne :vl-binary-lt :vl-binary-lte :vl-binary-gt :vl-binary-gte)))) nil) (a32p (eql asize 32)) (b32p (eql bsize 32)) ((unless (or a32p b32p)) type) ((mv expr-32 size-other) (if a32p (mv a bsize) (mv b asize))) (atoms (vl-expr-interesting-size-atoms expr-32)) (unsized (vl-collect-unsized-ints atoms)) (unsized-fit-p (nats-below-p (ash 1 size-other) (vl-exprlist-resolved->vals unsized))) ((unless unsized-fit-p) (intern-in-package-of-symbol (cat (symbol-name type) "-CONST-TOOBIG") type)) ((when (consp unsized)) (intern-in-package-of-symbol (cat (symbol-name type) "-MINOR") type))) type)))
Theorem:
(defthm symbolp-of-vl-tweak-fussy-warning-type (b* ((adjusted-type (vl-tweak-fussy-warning-type type a b asize bsize op))) (symbolp adjusted-type)) :rule-classes :type-prescription)
Theorem:
(defthm vl-tweak-fussy-warning-type-of-symbol-fix-type (equal (vl-tweak-fussy-warning-type (acl2::symbol-fix type) a b asize bsize op) (vl-tweak-fussy-warning-type type a b asize bsize op)))
Theorem:
(defthm vl-tweak-fussy-warning-type-symbol-equiv-congruence-on-type (implies (acl2::symbol-equiv type type-equiv) (equal (vl-tweak-fussy-warning-type type a b asize bsize op) (vl-tweak-fussy-warning-type type-equiv a b asize bsize op))) :rule-classes :congruence)
Theorem:
(defthm vl-tweak-fussy-warning-type-of-vl-expr-fix-a (equal (vl-tweak-fussy-warning-type type (vl-expr-fix a) b asize bsize op) (vl-tweak-fussy-warning-type type a b asize bsize op)))
Theorem:
(defthm vl-tweak-fussy-warning-type-vl-expr-equiv-congruence-on-a (implies (vl-expr-equiv a a-equiv) (equal (vl-tweak-fussy-warning-type type a b asize bsize op) (vl-tweak-fussy-warning-type type a-equiv b asize bsize op))) :rule-classes :congruence)
Theorem:
(defthm vl-tweak-fussy-warning-type-of-vl-expr-fix-b (equal (vl-tweak-fussy-warning-type type a (vl-expr-fix b) asize bsize op) (vl-tweak-fussy-warning-type type a b asize bsize op)))
Theorem:
(defthm vl-tweak-fussy-warning-type-vl-expr-equiv-congruence-on-b (implies (vl-expr-equiv b b-equiv) (equal (vl-tweak-fussy-warning-type type a b asize bsize op) (vl-tweak-fussy-warning-type type a b-equiv asize bsize op))) :rule-classes :congruence)
Theorem:
(defthm vl-tweak-fussy-warning-type-of-nfix-asize (equal (vl-tweak-fussy-warning-type type a b (nfix asize) bsize op) (vl-tweak-fussy-warning-type type a b asize bsize op)))
Theorem:
(defthm vl-tweak-fussy-warning-type-nat-equiv-congruence-on-asize (implies (acl2::nat-equiv asize asize-equiv) (equal (vl-tweak-fussy-warning-type type a b asize bsize op) (vl-tweak-fussy-warning-type type a b asize-equiv bsize op))) :rule-classes :congruence)
Theorem:
(defthm vl-tweak-fussy-warning-type-of-nfix-bsize (equal (vl-tweak-fussy-warning-type type a b asize (nfix bsize) op) (vl-tweak-fussy-warning-type type a b asize bsize op)))
Theorem:
(defthm vl-tweak-fussy-warning-type-nat-equiv-congruence-on-bsize (implies (acl2::nat-equiv bsize bsize-equiv) (equal (vl-tweak-fussy-warning-type type a b asize bsize op) (vl-tweak-fussy-warning-type type a b asize bsize-equiv op))) :rule-classes :congruence)
Theorem:
(defthm vl-tweak-fussy-warning-type-of-vl-op-fix-op (equal (vl-tweak-fussy-warning-type type a b asize bsize (vl-op-fix op)) (vl-tweak-fussy-warning-type type a b asize bsize op)))
Theorem:
(defthm vl-tweak-fussy-warning-type-vl-op-equiv-congruence-on-op (implies (vl-op-equiv op op-equiv) (equal (vl-tweak-fussy-warning-type type a b asize bsize op) (vl-tweak-fussy-warning-type type a b asize bsize op-equiv))) :rule-classes :congruence)