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__)) (vl-expr-case x :vl-literal (list (vl-expr-fix x)) :vl-index (list (vl-expr-fix x)) :vl-unary (case x.op ((:vl-unary-plus :vl-unary-minus :vl-unary-bitnot) (vl-expr-interesting-size-atoms x.arg)) ((:vl-unary-lognot :vl-unary-bitand :vl-unary-nand :vl-unary-bitor :vl-unary-nor :vl-unary-xor :vl-unary-xnor) nil) ((:vl-unary-preinc :vl-unary-predec :vl-unary-postinc :vl-unary-postdec) (vl-expr-interesting-size-atoms x.arg)) (otherwise (impossible))) :vl-binary (case x.op ((:vl-binary-logand :vl-binary-logor :vl-binary-lt :vl-binary-lte :vl-binary-gt :vl-binary-gte :vl-binary-eq :vl-binary-neq :vl-binary-ceq :vl-binary-cne :vl-binary-wildeq :vl-binary-wildneq :vl-implies :vl-equiv) nil) ((: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) (append (vl-expr-interesting-size-atoms x.left) (vl-expr-interesting-size-atoms x.right))) ((:vl-binary-power :vl-binary-shr :vl-binary-shl :vl-binary-ashr :vl-binary-ashl) (vl-expr-interesting-size-atoms x.left)) ((: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-expr-interesting-size-atoms x.left)) (otherwise (impossible))) :vl-qmark (append (vl-expr-interesting-size-atoms x.then) (vl-expr-interesting-size-atoms x.else)) :vl-concat nil :vl-multiconcat nil :vl-bitselect-expr nil :vl-partselect-expr nil :vl-mintypmax nil :vl-call nil :vl-stream nil :vl-cast (vl-casttype-case x.to :type nil :size nil :otherwise (vl-expr-interesting-size-atoms x.expr)) :vl-inside nil :vl-tagged nil :vl-pattern nil :vl-special nil :vl-eventexpr nil)))
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 (atom x) nil (append (vl-expr-interesting-size-atoms (car x)) (vl-exprlist-interesting-size-atoms (cdr x))))))
Theorem:
(defthm return-type-of-vl-expr-interesting-size-atoms.vals (b* ((?vals (vl-expr-interesting-size-atoms x))) (vl-exprlist-p vals)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-exprlist-interesting-size-atoms.vals (b* ((?vals (vl-exprlist-interesting-size-atoms x))) (vl-exprlist-p vals)) :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)