		Search-engine friendly clone of the ACL2 documentation.

Expr-tools

Vl-expr-typedecide

Determine the arithmetic class (signed or unsigned integer, shortreal or real, or something else) of an top-level or self-determined expression.

Signature
(vl-expr-typedecide x ss scopes) → (mv warnings class)
Arguments: x — Guard (vl-expr-p x).; ss — Guard (vl-scopestack-p ss).; scopes — Guard (vl-elabscopes-p scopes).
Returns: warnings — Type (vl-warninglist-p warnings).; class — Type (vl-arithclass-p class).

This function must only be used on "top-level" and self-determined portions of expressions. That is, consider an assignment like:

assign w = {foo + bar, a + b} | (baz + 1) ;

Here, it is legitimate to call vl-expr-typedecide to determine the arithmetic class of:

foo + bar, because it is self-determined,
a + b, because it is self-determined, and
{foo + bar, a + b} | (baz + 1), because it is top-level.

But it is not legitimate to try to decide the class of, baz + 1 in isolation, and doing so could yield an nonsensical result. For instance, if baz is signed then, by itself, baz + 1 looks like a signed addition. But concatenations are always unsigned, so in the larger context we can see that this addition is in fact unsigned.

The class we return is only a vl-arithclass-p. We might return an error class if there is some kind of actual error with the module or the expression, e.g., the use of a wire which is not declared; in these cases we add fatal warnings. But we may also encounter expressions whose type we do not know how to compute (e.g., perhaps the expression is an unsupported system call). In such cases we just return an error class without adding any warnings.

See vl2014::expression-sizing-minutia for many relevant notes on expression signedness.

Definitions and Theorems

Function: vl-expr-typedecide

(defun vl-expr-typedecide (x ss scopes)
 (declare (xargs :guard (and (vl-expr-p x)
                             (vl-scopestack-p ss)
                             (vl-elabscopes-p scopes))))
 (let ((__function__ 'vl-expr-typedecide))
  (declare (ignorable __function__))
  (b* ((x (vl-expr-fix x)) (warnings nil))
   (vl-expr-case
    x :vl-special (mv (ok) :vl-other-class)
    :vl-literal
    (mv (ok) (vl-value-typedecide x.val))
    :vl-index
    (vl-index-typedecide x ss scopes)
    :vl-unary
    (b* (((mv warnings arg-class)
          (vl-expr-typedecide x.arg ss scopes))
         ((wmv warnings ans)
          (vl-unaryop-typedecide x arg-class)))
      (mv warnings ans))
    :vl-binary
    (b* (((mv warnings left-class)
          (vl-expr-typedecide x.left ss scopes))
         ((wmv warnings right-class)
          (vl-expr-typedecide x.right ss scopes))
         ((wmv warnings ans)
          (vl-binaryop-typedecide x left-class right-class)))
      (mv warnings ans))
    :vl-qmark
    (b* (((mv warnings then-class)
          (vl-expr-typedecide x.then ss scopes))
         ((wmv warnings else-class)
          (vl-expr-typedecide x.else ss scopes)))
      (mv warnings
          (vl-arithclass-max then-class else-class)))
    :vl-mintypmax (mv (ok) :vl-other-class)
    :vl-concat
    (mv (ok) :vl-unsigned-int-class)
    :vl-multiconcat
    (mv (ok) :vl-unsigned-int-class)
    :vl-bitselect-expr
    (mv (ok) :vl-unsigned-int-class)
    :vl-partselect-expr
    (if (vl-partselect-case x.part :none)
        (vl-expr-typedecide x.subexp ss scopes)
      (mv (ok) :vl-unsigned-int-class))
    :vl-stream (mv (ok) :vl-other-class)
    :vl-call
    (if x.systemp (vl-syscall-typedecide x)
      (vl-funcall-typedecide x ss scopes))
    :vl-cast
    (vl-casttype-case
     x.to :type
     (b*
      (((mv err to-type)
        (vl-datatype-usertype-resolve x.to.type ss))
       ((when err)
        (mv
         (fatal
          :type :vl-typedecide-fail
          :msg
          "Failed to resolve usertypes for ~
                                          cast expression ~a0: ~@1."
          :args (list x err))
         :vl-error-class))
       ((unless (vl-datatype-packedp to-type))
        (mv (ok) :vl-other-class))
       ((mv ?caveat class)
        (vl-datatype-arithclass to-type)))
      (mv (ok) class))
     :signedness (mv (ok)
                     (if x.to.signedp :vl-signed-int-class
                       :vl-unsigned-int-class))
     :otherwise (vl-expr-typedecide x.expr ss scopes))
    :vl-inside
    (mv (ok) :vl-unsigned-int-class)
    :vl-tagged (mv (ok) :vl-other-class)
    :vl-pattern
    (b*
     (((unless x.pattype)
       (mv (ok) :vl-other-class))
      ((mv err pattype)
       (vl-datatype-usertype-resolve x.pattype ss))
      ((when err)
       (mv
        (fatal
         :type :vl-selfsize-fail
         :msg
         "Failed to resolve usertypes for ~
                                        pattern expression ~a0: ~@1"
         :args (list x err))
        :vl-error-class))
      ((unless (vl-datatype-packedp pattype))
       (mv (ok) :vl-other-class))
      ((mv ?caveat class)
       (vl-datatype-arithclass pattype)))
     (mv (ok) class))
    :vl-eventexpr (mv (ok) :vl-other-class)))))

Theorem: vl-warninglist-p-of-vl-expr-typedecide.warnings

(defthm vl-warninglist-p-of-vl-expr-typedecide.warnings
  (b* (((mv ?warnings common-lisp::?class)
        (vl-expr-typedecide x ss scopes)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-arithclass-p-of-vl-expr-typedecide.class

(defthm vl-arithclass-p-of-vl-expr-typedecide.class
  (b* (((mv ?warnings common-lisp::?class)
        (vl-expr-typedecide x ss scopes)))
    (vl-arithclass-p class))
  :rule-classes :rewrite)

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

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

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

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

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

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

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

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

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

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

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

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

Subtopics

Vl-arithclass-p: Classification of expressions (or datatypes) as signed or unsigned integral, shortreal, real, or of some other kind.
Vl-binaryop-typedecide
Vl-funcall-typedecide
Vl-index-typedecide
Vl-unaryop-typedecide
Vl-signedness-ambiguity-warning
Vl-syscall-typedecide
Vl-value-typedecide
Vl-operandinfo-signedness-caveat