		Search-engine friendly clone of the ACL2 documentation.

Vl-expr-size

Vl-expr-typedecide

Computation of expression signedness (main routine).

Signature
(vl-expr-typedecide x ss ctx warnings) → (mv warnings type)
Arguments: x — Guard (vl-expr-p x).; ss — Guard (vl-scopestack-p ss).; ctx — Guard (vl-context-p ctx).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings).; type — Type (and (vl-maybe-exprtype-p type) (equal (vl-exprtype-p type) (if type t nil))) .

Warning: this function should typically only be called by the expression-sizing transform.

We determine the signedness of an expression. 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 signs 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 sign 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 sign we return is only a vl-maybe-exprtype-p. We might return nil for two reasons. First, there could be 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 nil for the sign without adding any warnings.

Definitions and Theorems

Function: vl-expr-typedecide

(defun vl-expr-typedecide (x ss ctx warnings)
 (declare (xargs :guard (and (vl-expr-p x)
                             (vl-scopestack-p ss)
                             (vl-context-p ctx)
                             (vl-warninglist-p warnings))))
 (let ((__function__ 'vl-expr-typedecide))
  (declare (ignorable __function__))
  (b*
   ((x (vl-expr-fix x))
    (ctx (vl-context-fix ctx))
    ((mv warnings right-type)
     (vl-expr-typedecide-aux x ss ctx warnings :probably-right))
    ((mv warnings wrong-type)
     (vl-expr-typedecide-aux x ss ctx warnings :probably-wrong))
    (warnings
     (if (eq right-type wrong-type)
         warnings
      (warn
       :type :vl-warn-vague-spec
       :msg
       "~a0: expression ~a1 has a type which is not necessarily ~
                      clear according to the discussion in the Verilog-2005 ~
                      standard.  We believe its type should be ~s2, but think ~
                      it would be easy for other Verilog systems to ~
                      mistakenly interpret the expression as ~s3.  To reduce ~
                      any potential confusion, you may wish to rewrite this ~
                      expression to make its signedness unambiguous.  Some ~
                      typical causes of signedness are plain decimal numbers ~
                      like 10, and the use of integer variables instead of ~
                      regs."
       :args (list ctx x right-type wrong-type)))))
   (mv warnings right-type))))

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

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

Theorem: return-type-of-vl-expr-typedecide.type

(defthm return-type-of-vl-expr-typedecide.type
  (b* (((mv ?warnings common-lisp::?type)
        (vl-expr-typedecide x ss ctx warnings)))
    (and (vl-maybe-exprtype-p type)
         (equal (vl-exprtype-p type)
                (if type t nil))))
  :rule-classes :rewrite)

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

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

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

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

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

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

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

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

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

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

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

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

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

Subtopics

Vl-expr-typedecide-aux: Core of computing expression signedness.
Vl-atom-typedecide: Effectively computes the "self-determined" type of an atom.
Vl-warn-about-signed-shifts: Special warnings about shifting by signed amounts.
Vl-datatype-exprtype: Get the self-determined type for a datatype.
Vl-exprtype-max: (vl-exprtype-max x y &rest rst) is given vl-exprtype-ps as arguments; it returns :vl-unsigned if any argument is unsigned, or :vl-signed when all arguments are signed.