Computation of expression signedness (main routine).
(vl-expr-typedecide x ss ctx warnings) → (mv warnings type)
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
But it is not legitimate to try to decide the sign of,
The
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)