		Search-engine friendly clone of the ACL2 documentation.

Expr-tools

Vl-expr-selfsize

Computation of self-determined expression sizes.

Signature
(vl-expr-selfsize x ss scopes) → (mv warnings size)
Arguments: x — Expression whose size we are to compute.
Guard (vl-expr-p x).; ss — Scope where the expression occurs.
Guard (vl-scopestack-p ss).; scopes — Precomputed overrides for parameter and function types.
Guard (vl-elabscopes-p scopes).
Returns: warnings — Type (vl-warninglist-p warnings).; size — Type (maybe-natp size).

Some failures are expected, e.g., we do not know how to size some system calls. In these cases we do not cause any warnings. But in other cases, a failure might mean that the expression is malformed in some way, e.g., maybe it references an undefined wire or contains a raw, "unindexed" reference to an array. In these cases we generate fatal warnings.

Theorem: return-type-of-vl-expr-selfsize.warnings

(defthm return-type-of-vl-expr-selfsize.warnings
        (b* (((mv ?warnings ?size)
              (vl-expr-selfsize x ss scopes)))
            (vl-warninglist-p warnings))
        :rule-classes :rewrite)

Theorem: return-type-of-vl-expr-selfsize.size

(defthm return-type-of-vl-expr-selfsize.size
        (b* (((mv ?warnings ?size)
              (vl-expr-selfsize x ss scopes)))
            (maybe-natp size))
        :rule-classes :type-prescription)

Theorem: return-type-of-vl-exprlist-selfsize.warnings

(defthm return-type-of-vl-exprlist-selfsize.warnings
        (b* (((mv ?warnings ?sizes)
              (vl-exprlist-selfsize x ss scopes)))
            (vl-warninglist-p warnings))
        :rule-classes :rewrite)

Theorem: return-type-of-vl-exprlist-selfsize.sizes

(defthm return-type-of-vl-exprlist-selfsize.sizes
        (b* (((mv ?warnings ?sizes)
              (vl-exprlist-selfsize x ss scopes)))
            (maybe-nat-list-p sizes))
        :rule-classes :rewrite)

Theorem: vl-expr-selfsize-of-vl-expr-fix-x

(defthm vl-expr-selfsize-of-vl-expr-fix-x
        (equal (vl-expr-selfsize (vl-expr-fix x)
                                 ss scopes)
               (vl-expr-selfsize x ss scopes)))

Theorem: vl-expr-selfsize-of-vl-scopestack-fix-ss

(defthm vl-expr-selfsize-of-vl-scopestack-fix-ss
        (equal (vl-expr-selfsize x (vl-scopestack-fix ss)
                                 scopes)
               (vl-expr-selfsize x ss scopes)))

Theorem: vl-expr-selfsize-of-vl-elabscopes-fix-scopes

(defthm vl-expr-selfsize-of-vl-elabscopes-fix-scopes
        (equal (vl-expr-selfsize x ss (vl-elabscopes-fix scopes))
               (vl-expr-selfsize x ss scopes)))

Theorem: vl-exprlist-selfsize-of-vl-exprlist-fix-x

(defthm vl-exprlist-selfsize-of-vl-exprlist-fix-x
        (equal (vl-exprlist-selfsize (vl-exprlist-fix x)
                                     ss scopes)
               (vl-exprlist-selfsize x ss scopes)))

Theorem: vl-exprlist-selfsize-of-vl-scopestack-fix-ss

(defthm vl-exprlist-selfsize-of-vl-scopestack-fix-ss
        (equal (vl-exprlist-selfsize x (vl-scopestack-fix ss)
                                     scopes)
               (vl-exprlist-selfsize x ss scopes)))

Theorem: vl-exprlist-selfsize-of-vl-elabscopes-fix-scopes

(defthm
     vl-exprlist-selfsize-of-vl-elabscopes-fix-scopes
     (equal (vl-exprlist-selfsize x ss (vl-elabscopes-fix scopes))
            (vl-exprlist-selfsize x ss scopes)))

Theorem: vl-expr-selfsize-vl-expr-equiv-congruence-on-x

(defthm vl-expr-selfsize-vl-expr-equiv-congruence-on-x
        (implies (vl-expr-equiv x x-equiv)
                 (equal (vl-expr-selfsize x ss scopes)
                        (vl-expr-selfsize x-equiv ss scopes)))
        :rule-classes :congruence)

Theorem: vl-expr-selfsize-vl-scopestack-equiv-congruence-on-ss

(defthm vl-expr-selfsize-vl-scopestack-equiv-congruence-on-ss
        (implies (vl-scopestack-equiv ss ss-equiv)
                 (equal (vl-expr-selfsize x ss scopes)
                        (vl-expr-selfsize x ss-equiv scopes)))
        :rule-classes :congruence)

Theorem: vl-expr-selfsize-vl-elabscopes-equiv-congruence-on-scopes

(defthm vl-expr-selfsize-vl-elabscopes-equiv-congruence-on-scopes
        (implies (vl-elabscopes-equiv scopes scopes-equiv)
                 (equal (vl-expr-selfsize x ss scopes)
                        (vl-expr-selfsize x ss scopes-equiv)))
        :rule-classes :congruence)

Theorem: vl-exprlist-selfsize-vl-exprlist-equiv-congruence-on-x

(defthm vl-exprlist-selfsize-vl-exprlist-equiv-congruence-on-x
        (implies (vl-exprlist-equiv x x-equiv)
                 (equal (vl-exprlist-selfsize x ss scopes)
                        (vl-exprlist-selfsize x-equiv ss scopes)))
        :rule-classes :congruence)

Theorem: vl-exprlist-selfsize-vl-scopestack-equiv-congruence-on-ss

(defthm vl-exprlist-selfsize-vl-scopestack-equiv-congruence-on-ss
        (implies (vl-scopestack-equiv ss ss-equiv)
                 (equal (vl-exprlist-selfsize x ss scopes)
                        (vl-exprlist-selfsize x ss-equiv scopes)))
        :rule-classes :congruence)

Theorem: vl-exprlist-selfsize-vl-elabscopes-equiv-congruence-on-scopes

(defthm
     vl-exprlist-selfsize-vl-elabscopes-equiv-congruence-on-scopes
     (implies (vl-elabscopes-equiv scopes scopes-equiv)
              (equal (vl-exprlist-selfsize x ss scopes)
                     (vl-exprlist-selfsize x ss scopes-equiv)))
     :rule-classes :congruence)

Subtopics

Vl-tweak-fussy-warning-type: Heuristically categorize fussy warnings according to severity.
Vl-binaryop-selfsize: Main function for computing self-determined expression sizes.
Vl-expr-opacity: Returns the "opacity" of the expression, a way of categorizing the expression for sizing.
Vl-unaryop-selfsize: Main function for computing self-determined expression sizes.
Vl-exprlist-selfsize