Heuristic for deciding whether to issue truncation warnings.
(vl-okay-to-truncate-expr width x ss) → *
Function:
(defun vl-okay-to-truncate-expr (width x ss) (declare (xargs :guard (and (natp width) (vl-expr-p x) (vl-scopestack-p ss)))) (let ((__function__ 'vl-okay-to-truncate-expr)) (declare (ignorable __function__)) (let* ((width (nfix width)) (x (vl-expr-fix x)) (ss (vl-scopestack-fix ss))) (vl-expr-case x :vl-literal (vl-value-case x.val (:vl-constint (or (and x.val.wasunsized (= x.val.origwidth 32) (not (logbitp 31 x.val.value)) (< x.val.value (ash 1 width))) (and (vl-exprsign-equiv x.val.origsign :vl-unsigned) (< x.val.value (ash 1 width))) (and (assoc-equal "VL_PARAMNAME" x.atts) (< x.val.value (ash 1 width))))) (:otherwise nil)) :vl-index (vl-unsized-index-p x ss) :vl-binary (and (vl-binaryop-equiv x.op :vl-binary-rem) (b* ((k (and (vl-expr-resolved-p x.right) (vl-resolved->val x.right))) (max (ash 1 width))) (and k (<= k max)))) :vl-qmark (and (vl-okay-to-truncate-expr width x.then ss) (vl-okay-to-truncate-expr width x.else ss)) :vl-call (vl-is-integer-valued-syscall x) :vl-multiconcat (vl-expr-is-{n{0}}-p x) :otherwise nil))))
Theorem:
(defthm vl-okay-to-truncate-expr-of-nfix-width (equal (vl-okay-to-truncate-expr (nfix width) x ss) (vl-okay-to-truncate-expr width x ss)))
Theorem:
(defthm vl-okay-to-truncate-expr-nat-equiv-congruence-on-width (implies (acl2::nat-equiv width width-equiv) (equal (vl-okay-to-truncate-expr width x ss) (vl-okay-to-truncate-expr width-equiv x ss))) :rule-classes :congruence)
Theorem:
(defthm vl-okay-to-truncate-expr-of-vl-expr-fix-x (equal (vl-okay-to-truncate-expr width (vl-expr-fix x) ss) (vl-okay-to-truncate-expr width x ss)))
Theorem:
(defthm vl-okay-to-truncate-expr-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-okay-to-truncate-expr width x ss) (vl-okay-to-truncate-expr width x-equiv ss))) :rule-classes :congruence)
Theorem:
(defthm vl-okay-to-truncate-expr-of-vl-scopestack-fix-ss (equal (vl-okay-to-truncate-expr width x (vl-scopestack-fix ss)) (vl-okay-to-truncate-expr width x ss)))
Theorem:
(defthm vl-okay-to-truncate-expr-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-okay-to-truncate-expr width x ss) (vl-okay-to-truncate-expr width x ss-equiv))) :rule-classes :congruence)