Compute the self-determined size of an atom.
(vl-atom-selfsize x ss ctx warnings) → (mv warnings size)
Warning: this function should typically only be called by the expression-sizing transform.
We attempt to compute the "self-determined size" of the atom
We have taken special care in our lexer to ensure that every constant, whether it is a vl-weirdint-p or vl-constint-p, has a determined width. As a result, it is easy to determine the self-determined size of a constant, and we never fail to do so.
For identifiers, we must look up the identifier in the module to try to
determine its size. This can fail if the identifier is not declared in the
module, or if its size is not resolved. In these cases, we add a fatal warning
to
We do not try to size other atoms, such as real numbers, individual HID
pieces, function names, system function names, etc.; instead we just return
Function:
(defun vl-atom-selfsize (x ss ctx warnings) (declare (xargs :guard (and (vl-expr-p x) (vl-scopestack-p ss) (vl-context-p ctx) (vl-warninglist-p warnings)))) (declare (xargs :guard (vl-atom-p x))) (let ((__function__ 'vl-atom-selfsize)) (declare (ignorable __function__)) (b* ((x (vl-expr-fix x)) (ctx (vl-context-fix ctx)) (guts (vl-atom->guts x)) ((when (vl-fast-constint-p guts)) (mv (ok) (vl-constint->origwidth guts))) ((when (vl-fast-weirdint-p guts)) (mv (ok) (vl-weirdint->origwidth guts))) ((when (vl-fast-string-p guts)) (mv (ok) (* 8 (length (vl-string->value guts))))) ((when (eq (tag guts) :vl-extint)) (mv (ok) 1)) ((unless (or (vl-fast-id-p guts) (vl-fast-hidpiece-p guts))) (mv (ok) nil))) (vl-index-selfsize x ss ctx warnings))))
Theorem:
(defthm vl-warninglist-p-of-vl-atom-selfsize.warnings (b* (((mv ?warnings ?size) (vl-atom-selfsize x ss ctx warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm maybe-natp-of-vl-atom-selfsize.size (b* (((mv ?warnings ?size) (vl-atom-selfsize x ss ctx warnings))) (maybe-natp size)) :rule-classes :type-prescription)
Theorem:
(defthm warning-irrelevance-of-vl-atom-selfsize (let ((ret1 (vl-atom-selfsize x ss ctx warnings)) (ret2 (vl-atom-selfsize x ss nil nil))) (implies (syntaxp (not (and (equal ctx ''nil) (equal warnings ''nil)))) (equal (mv-nth 1 ret1) (mv-nth 1 ret2)))))
Theorem:
(defthm vl-atom-selfsize-of-vl-expr-fix-x (equal (vl-atom-selfsize (vl-expr-fix x) ss ctx warnings) (vl-atom-selfsize x ss ctx warnings)))
Theorem:
(defthm vl-atom-selfsize-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-atom-selfsize x ss ctx warnings) (vl-atom-selfsize x-equiv ss ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-atom-selfsize-of-vl-scopestack-fix-ss (equal (vl-atom-selfsize x (vl-scopestack-fix ss) ctx warnings) (vl-atom-selfsize x ss ctx warnings)))
Theorem:
(defthm vl-atom-selfsize-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-atom-selfsize x ss ctx warnings) (vl-atom-selfsize x ss-equiv ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-atom-selfsize-of-vl-context-fix-ctx (equal (vl-atom-selfsize x ss (vl-context-fix ctx) warnings) (vl-atom-selfsize x ss ctx warnings)))
Theorem:
(defthm vl-atom-selfsize-vl-context-equiv-congruence-on-ctx (implies (vl-context-equiv ctx ctx-equiv) (equal (vl-atom-selfsize x ss ctx warnings) (vl-atom-selfsize x ss ctx-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-atom-selfsize-of-vl-warninglist-fix-warnings (equal (vl-atom-selfsize x ss ctx (vl-warninglist-fix warnings)) (vl-atom-selfsize x ss ctx warnings)))
Theorem:
(defthm vl-atom-selfsize-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-atom-selfsize x ss ctx warnings) (vl-atom-selfsize x ss ctx warnings-equiv))) :rule-classes :congruence)