		Search-engine friendly clone of the ACL2 documentation.

Expression-sizing

Vl-expr-size

Determine sizes for a top-level or self-determined expression.

Signature
(vl-expr-size lhs-size x ss ctx warnings) → (mv successp warnings new-x)
Arguments: lhs-size — To size an expression x which occurs in an assignment such as assign lhs = x, the lhs-size should be the width of lhs. To size other expressions that do not occur in assignments, such as a self-determined subexpression, the lhs-size should be nil.
Guard (maybe-natp lhs-size).; x — The expression that we want to size.
Guard (vl-expr-p x).; ss — Guard (vl-scopestack-p ss).; ctx — Context for sizing error messages.
Guard (vl-context-p ctx).; warnings — Ordinary warnings accumulator.
Guard (vl-warninglist-p warnings).
Returns: successp — Indicates whether all sizing was successful.
Type (booleanp successp).; warnings — Possibly extended with fatal or non-fatal warnings.
Type (vl-warninglist-p warnings).; new-x — Updated version of x where all the sizes/types have been computed and installed.
Type (vl-expr-p new-x).

This function implements the two-phase algorithm described in expression-sizing. That is, it first determines the maximum size of any operand in x and the desired type of x, using vl-expr-selfsize and vl-expr-typedecide (which are not part of the mutual recursion). It then propagates this size and type into the operands, using vl-expr-expandsizes.

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

(defthm return-type-of-vl-expr-size.successp
  (b* (((mv ?successp ?warnings ?new-x)
        (vl-expr-size lhs-size x ss ctx warnings)))
    (booleanp successp))
  :rule-classes :type-prescription)

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

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

Theorem: return-type-of-vl-expr-size.new-x

(defthm return-type-of-vl-expr-size.new-x
  (b* (((mv ?successp ?warnings ?new-x)
        (vl-expr-size lhs-size x ss ctx warnings)))
    (vl-expr-p new-x))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-exprlist-size.successp

(defthm return-type-of-vl-exprlist-size.successp
  (b* (((mv ?successp ?warnings ?new-x)
        (vl-exprlist-size x ss ctx warnings)))
    (booleanp successp))
  :rule-classes :type-prescription)

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

(defthm return-type-of-vl-exprlist-size.warnings
  (b* (((mv ?successp ?warnings ?new-x)
        (vl-exprlist-size x ss ctx warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-exprlist-size.new-x

(defthm return-type-of-vl-exprlist-size.new-x
  (b* (((mv ?successp ?warnings ?new-x)
        (vl-exprlist-size x ss ctx warnings)))
    (and (vl-exprlist-p new-x)
         (equal (len new-x) (len x))))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-exprlist-expandsizes.successp

(defthm return-type-of-vl-exprlist-expandsizes.successp
 (b*
  (((mv ?successp ?warnings ?new-x)
    (vl-exprlist-expandsizes x
                             finalwidth finaltype ss ctx warnings)))
  (booleanp successp))
 :rule-classes :type-prescription)

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

(defthm return-type-of-vl-exprlist-expandsizes.warnings
 (b*
  (((mv ?successp ?warnings ?new-x)
    (vl-exprlist-expandsizes x
                             finalwidth finaltype ss ctx warnings)))
  (vl-warninglist-p warnings))
 :rule-classes :rewrite)

Theorem: return-type-of-vl-exprlist-expandsizes.new-x

(defthm return-type-of-vl-exprlist-expandsizes.new-x
 (b*
  (((mv ?successp ?warnings ?new-x)
    (vl-exprlist-expandsizes x
                             finalwidth finaltype ss ctx warnings)))
  (and (vl-exprlist-p new-x)
       (equal (len new-x) (len x))))
 :rule-classes :rewrite)

Theorem: return-type-of-vl-expr-expandsizes.successp

(defthm return-type-of-vl-expr-expandsizes.successp
  (b* (((mv ?successp ?warnings ?new-x)
        (vl-expr-expandsizes x
                             finalwidth finaltype ss ctx warnings)))
    (booleanp successp))
  :rule-classes :type-prescription)

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

(defthm return-type-of-vl-expr-expandsizes.warnings
  (b* (((mv ?successp ?warnings ?new-x)
        (vl-expr-expandsizes x
                             finalwidth finaltype ss ctx warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-expr-expandsizes.new-x

(defthm return-type-of-vl-expr-expandsizes.new-x
  (b* (((mv ?successp ?warnings ?new-x)
        (vl-expr-expandsizes x
                             finalwidth finaltype ss ctx warnings)))
    (vl-expr-p new-x))
  :rule-classes :rewrite)

Subtopics

Vl-expr-selfsize: Computation of self-determined expression sizes.
Vl-expr-typedecide: Computation of expression signedness (main routine).
Vl-expr-expandsizes: Propagate the final width/type into a context-determined expression.
Vl-exprlist-expandsizes: Propagate final width/type into a list of context-determined expressions.
Vl-exprlist-size: Self-determine the sizes of a list of expressions.