		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