Heuristically categorize fussy warnings according to severity.
(vl-tweak-fussy-warning-type type a b asize bsize op ss scopes) → 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 ss scopes) (declare (xargs :guard (and (symbolp type) (vl-expr-p a) (vl-expr-p b) (natp asize) (natp bsize) (symbolp op) (vl-scopestack-p ss) (vl-elabscopes-p scopes)))) (let ((__function__ 'vl-tweak-fussy-warning-type)) (declare (ignorable __function__)) (b* ((type (acl2::symbol-fix type)) (op (acl2::symbol-fix op)) (asize (lnfix asize)) (bsize (lnfix bsize)) (ss (vl-scopestack-fix ss)) (scopes (vl-elabscopes-fix scopes)) (a (vl-tweak-fussy-warning-type-preclean a)) (b (vl-tweak-fussy-warning-type-preclean b)) ((mv a asize) (vl-tweak-fussy-warning-expr-size a asize)) ((mv b bsize) (vl-tweak-fussy-warning-expr-size b bsize)) ((when (equal asize bsize)) nil) (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-fussy-may-as-well-be-extint-p a) (vl-fussy-may-as-well-be-extint-p b))) nil) ((when (vl-suppress-fussy-warning-for-shift-of-mask op a b)) nil) (a-fits-b-p (and (vl-expr-resolved-p a) (or (unsigned-byte-p bsize (vl-resolved->val a)) (and (< 0 bsize) (signed-byte-p bsize (vl-resolved->val a)))))) (b-fits-a-p (and (vl-expr-resolved-p b) (or (unsigned-byte-p asize (vl-resolved->val b)) (and (< 0 asize) (signed-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) (a-plusp (vl-expr-case a :vl-binary (vl-tweak-fussy-warning-type-arithop a.op) :otherwise nil)) (b-plusp (vl-expr-case b :vl-binary (vl-tweak-fussy-warning-type-arithop b.op) :otherwise nil)) (ret-type (if (if (< asize bsize) a-plusp b-plusp) (intern-in-package-of-symbol (cat (symbol-name type) "-MINOR") type) type)) (a32p (eql asize 32)) (b32p (eql bsize 32)) ((unless (or a32p b32p)) ret-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 ss scopes)) (unsized-vals (vl-exprlist-resolved->vals (vl-collect-resolved-exprs unsized))) (unsized-fit-p (ints-probably-fit-p size-other unsized-vals)) ((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-INTSIZE") type))) ret-type)))
Theorem:
(defthm symbolp-of-vl-tweak-fussy-warning-type (b* ((adjusted-type (vl-tweak-fussy-warning-type type a b asize bsize op ss scopes))) (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 ss scopes) (vl-tweak-fussy-warning-type type a b asize bsize op ss scopes)))
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 ss scopes) (vl-tweak-fussy-warning-type type-equiv a b asize bsize op ss scopes))) :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 ss scopes) (vl-tweak-fussy-warning-type type a b asize bsize op ss scopes)))
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 ss scopes) (vl-tweak-fussy-warning-type type a-equiv b asize bsize op ss scopes))) :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 ss scopes) (vl-tweak-fussy-warning-type type a b asize bsize op ss scopes)))
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 ss scopes) (vl-tweak-fussy-warning-type type a b-equiv asize bsize op ss scopes))) :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 ss scopes) (vl-tweak-fussy-warning-type type a b asize bsize op ss scopes)))
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 ss scopes) (vl-tweak-fussy-warning-type type a b asize-equiv bsize op ss scopes))) :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 ss scopes) (vl-tweak-fussy-warning-type type a b asize bsize op ss scopes)))
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 ss scopes) (vl-tweak-fussy-warning-type type a b asize bsize-equiv op ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-tweak-fussy-warning-type-of-symbol-fix-op (equal (vl-tweak-fussy-warning-type type a b asize bsize (acl2::symbol-fix op) ss scopes) (vl-tweak-fussy-warning-type type a b asize bsize op ss scopes)))
Theorem:
(defthm vl-tweak-fussy-warning-type-symbol-equiv-congruence-on-op (implies (acl2::symbol-equiv op op-equiv) (equal (vl-tweak-fussy-warning-type type a b asize bsize op ss scopes) (vl-tweak-fussy-warning-type type a b asize bsize op-equiv ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-tweak-fussy-warning-type-of-vl-scopestack-fix-ss (equal (vl-tweak-fussy-warning-type type a b asize bsize op (vl-scopestack-fix ss) scopes) (vl-tweak-fussy-warning-type type a b asize bsize op ss scopes)))
Theorem:
(defthm vl-tweak-fussy-warning-type-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-tweak-fussy-warning-type type a b asize bsize op ss scopes) (vl-tweak-fussy-warning-type type a b asize bsize op ss-equiv scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-tweak-fussy-warning-type-of-vl-elabscopes-fix-scopes (equal (vl-tweak-fussy-warning-type type a b asize bsize op ss (vl-elabscopes-fix scopes)) (vl-tweak-fussy-warning-type type a b asize bsize op ss scopes)))
Theorem:
(defthm vl-tweak-fussy-warning-type-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-tweak-fussy-warning-type type a b asize bsize op ss scopes) (vl-tweak-fussy-warning-type type a b asize bsize op ss scopes-equiv))) :rule-classes :congruence)