		Search-engine friendly clone of the ACL2 documentation.

Vl-expr-size

Vl-expr-selfsize

Computation of self-determined expression sizes.

Signature
(vl-expr-selfsize x ss ctx warnings) → (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).; ctx — Context for warnings.
Guard (vl-context-p ctx).; warnings — Ordinary warnings accumulator.
Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).; size — Type (maybe-natp size).

Warning: these functions should typically only be called by the expression-sizing transform.

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.

BOZO we might eventually add as inputs the full list of modules and a modalist so that we can look up HIDs. An alternative would be to use the annotations left by transforms such as the now-defunct vl-design-follow-hids, e.g., VL_HID_RESOLVED_RANGE_P, to see how wide HIDs are.

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 ctx warnings)))
    (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 ctx warnings)))
    (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 ?size-list)
        (vl-exprlist-selfsize x ss ctx warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-exprlist-selfsize.size-list

(defthm return-type-of-vl-exprlist-selfsize.size-list
  (b* (((mv ?warnings ?size-list)
        (vl-exprlist-selfsize x ss ctx warnings)))
    (and (vl-maybe-nat-listp size-list)
         (equal (len size-list) (len x))))
  :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 ctx warnings)
         (vl-expr-selfsize x ss ctx warnings)))

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)
                           ctx warnings)
         (vl-expr-selfsize x ss ctx warnings)))

Theorem: vl-expr-selfsize-of-vl-context-fix-ctx

(defthm vl-expr-selfsize-of-vl-context-fix-ctx
  (equal (vl-expr-selfsize x ss (vl-context-fix ctx)
                           warnings)
         (vl-expr-selfsize x ss ctx warnings)))

Theorem: vl-expr-selfsize-of-vl-warninglist-fix-warnings

(defthm vl-expr-selfsize-of-vl-warninglist-fix-warnings
  (equal (vl-expr-selfsize x ss ctx (vl-warninglist-fix warnings))
         (vl-expr-selfsize x ss ctx warnings)))

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 ctx warnings)
         (vl-exprlist-selfsize x ss ctx warnings)))

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)
                               ctx warnings)
         (vl-exprlist-selfsize x ss ctx warnings)))

Theorem: vl-exprlist-selfsize-of-vl-context-fix-ctx

(defthm vl-exprlist-selfsize-of-vl-context-fix-ctx
  (equal (vl-exprlist-selfsize x ss (vl-context-fix ctx)
                               warnings)
         (vl-exprlist-selfsize x ss ctx warnings)))

Theorem: vl-exprlist-selfsize-of-vl-warninglist-fix-warnings

(defthm vl-exprlist-selfsize-of-vl-warninglist-fix-warnings
  (equal
       (vl-exprlist-selfsize x ss ctx (vl-warninglist-fix warnings))
       (vl-exprlist-selfsize x ss ctx warnings)))

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 ctx warnings)
                  (vl-expr-selfsize x-equiv ss ctx warnings)))
  :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 ctx warnings)
                  (vl-expr-selfsize x ss-equiv ctx warnings)))
  :rule-classes :congruence)

Theorem: vl-expr-selfsize-vl-context-equiv-congruence-on-ctx

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

Theorem: vl-expr-selfsize-vl-warninglist-equiv-congruence-on-warnings

(defthm vl-expr-selfsize-vl-warninglist-equiv-congruence-on-warnings
  (implies (vl-warninglist-equiv warnings warnings-equiv)
           (equal (vl-expr-selfsize x ss ctx warnings)
                  (vl-expr-selfsize x ss ctx warnings-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 ctx warnings)
                  (vl-exprlist-selfsize x-equiv ss ctx warnings)))
  :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 ctx warnings)
                  (vl-exprlist-selfsize x ss-equiv ctx warnings)))
  :rule-classes :congruence)

Theorem: vl-exprlist-selfsize-vl-context-equiv-congruence-on-ctx

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

Theorem: vl-exprlist-selfsize-vl-warninglist-equiv-congruence-on-warnings

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

Theorem: warning-irrelevance-of-vl-expr-selfsize

(defthm warning-irrelevance-of-vl-expr-selfsize
  (let ((ret1 (vl-expr-selfsize x ss ctx warnings))
        (ret2 (vl-expr-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: warning-irrelevance-of-vl-exprlist-selfsize

(defthm warning-irrelevance-of-vl-exprlist-selfsize
  (let ((ret1 (vl-exprlist-selfsize x ss ctx warnings))
        (ret2 (vl-exprlist-selfsize x ss nil nil)))
    (implies (syntaxp (not (and (equal ctx ''nil)
                                (equal warnings ''nil))))
             (equal (mv-nth 1 ret1)
                    (mv-nth 1 ret2)))))

Subtopics

Vl-op-selfsize: Main function for computing self-determined expression sizes.
Vl-atom-selfsize: Compute the self-determined size of an atom.
Vl-exprlist-selfsize