Heuristic for tweaking fussy size warnings.
Our basic goal is to gather all the atoms throughout an expression that are "relevant" to the current self-size computation. This is a fuzzy concept and you should never use it for anything semantically meaningful, it's only meant as a heuristic for generating more useful warnings.
Function:
(defun vl-expr-interesting-size-atoms (x) (declare (xargs :guard (vl-expr-p x))) (let ((__function__ 'vl-expr-interesting-size-atoms)) (declare (ignorable __function__)) (b* ((x (vl-expr-fix x)) ((when (vl-fast-atom-p x)) (list x)) (op (vl-nonatom->op x)) (args (vl-nonatom->args x))) (case op ((:vl-bitselect :vl-unary-bitand :vl-unary-nand :vl-unary-bitor :vl-unary-nor :vl-unary-xor :vl-unary-xnor :vl-unary-lognot :vl-binary-logand :vl-binary-logor :vl-binary-eq :vl-binary-neq :vl-binary-ceq :vl-binary-cne :vl-binary-lt :vl-binary-lte :vl-binary-gt :vl-binary-gte :vl-partselect-colon :vl-partselect-pluscolon :vl-partselect-minuscolon :vl-select-colon :vl-select-pluscolon :vl-select-minuscolon :vl-syscall :vl-funcall :vl-mintypmax :vl-hid-dot :vl-index :vl-scope :vl-with-index :vl-with-colon :vl-with-pluscolon :vl-with-minuscolon :vl-stream-left :vl-stream-right :vl-stream-left-sized :vl-stream-right-sized :vl-tagged :vl-binary-wildeq :vl-binary-wildneq :vl-implies :vl-equiv :vl-binary-cast :vl-pattern-multi :vl-pattern-type :vl-pattern-positional :vl-pattern-keyvalue :vl-keyvalue :vl-unary-preinc :vl-unary-predec :vl-unary-postinc :vl-unary-postdec :vl-binary-assign :vl-binary-plusassign :vl-binary-minusassign :vl-binary-timesassign :vl-binary-divassign :vl-binary-remassign :vl-binary-andassign :vl-binary-orassign :vl-binary-xorassign :vl-binary-shlassign :vl-binary-shrassign :vl-binary-ashlassign :vl-binary-ashrassign :vl-inside :vl-valuerange :vl-valuerangelist) nil) ((:vl-binary-power :vl-unary-plus :vl-unary-minus :vl-unary-bitnot :vl-binary-shl :vl-binary-shr :vl-binary-ashl :vl-binary-ashr) (vl-expr-interesting-size-atoms (first args))) ((:vl-qmark :vl-multiconcat) (vl-exprlist-interesting-size-atoms (cdr args))) ((:vl-binary-plus :vl-binary-minus :vl-binary-times :vl-binary-div :vl-binary-rem :vl-binary-bitand :vl-binary-bitor :vl-binary-xor :vl-binary-xnor :vl-concat) (vl-exprlist-interesting-size-atoms args)) (otherwise (impossible))))))
Function:
(defun vl-exprlist-interesting-size-atoms (x) (declare (xargs :guard (vl-exprlist-p x))) (let ((__function__ 'vl-exprlist-interesting-size-atoms)) (declare (ignorable __function__)) (if (consp x) (append (vl-expr-interesting-size-atoms (car x)) (vl-exprlist-interesting-size-atoms (cdr x))) nil)))
Theorem:
(defthm return-type-of-vl-expr-interesting-size-atoms.exprs (b* ((?exprs (vl-expr-interesting-size-atoms x))) (and (vl-exprlist-p exprs) (vl-atomlist-p exprs))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-exprlist-interesting-size-atoms.exprs (b* ((?exprs (vl-exprlist-interesting-size-atoms x))) (and (vl-exprlist-p exprs) (vl-atomlist-p exprs))) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-expr-interesting-size-atoms (true-listp (vl-expr-interesting-size-atoms x)) :rule-classes :type-prescription)
Theorem:
(defthm true-listp-of-vl-exprlist-interesting-size-atoms (true-listp (vl-exprlist-interesting-size-atoms x)) :rule-classes :type-prescription)
Theorem:
(defthm vl-expr-interesting-size-atoms-of-vl-expr-fix-x (equal (vl-expr-interesting-size-atoms (vl-expr-fix x)) (vl-expr-interesting-size-atoms x)))
Theorem:
(defthm vl-exprlist-interesting-size-atoms-of-vl-exprlist-fix-x (equal (vl-exprlist-interesting-size-atoms (vl-exprlist-fix x)) (vl-exprlist-interesting-size-atoms x)))
Theorem:
(defthm vl-expr-interesting-size-atoms-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-expr-interesting-size-atoms x) (vl-expr-interesting-size-atoms x-equiv))) :rule-classes :congruence)
Theorem:
(defthm vl-exprlist-interesting-size-atoms-vl-exprlist-equiv-congruence-on-x (implies (vl-exprlist-equiv x x-equiv) (equal (vl-exprlist-interesting-size-atoms x) (vl-exprlist-interesting-size-atoms x-equiv))) :rule-classes :congruence)