		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucid-dissect-var-main

Signature
(vl-lucid-dissect-var-main ss item used set db genp) → (mv warnings possible-typop)
Arguments: ss — Guard (vl-scopestack-p ss).; item — Guard (or (vl-paramdecl-p item) (vl-vardecl-p item)).; used — Guard (vl-lucidocclist-p used).; set — Guard (vl-lucidocclist-p set).; db — Guard (vl-luciddb-p db).; genp — Guard (booleanp genp).
Returns: warnings — Type (vl-warninglist-p warnings).; possible-typop — Is this wire a typo-detection candidate? (Our idea is to focus on wires that are introduced implicitly and either unset or unused.).
Type (booleanp possible-typop).

Definitions and Theorems

Function: vl-lucid-dissect-var-main

(defun vl-lucid-dissect-var-main (ss item used set db genp)
 (declare (xargs :guard (and (vl-scopestack-p ss)
                             (or (vl-paramdecl-p item)
                                 (vl-vardecl-p item))
                             (vl-lucidocclist-p used)
                             (vl-lucidocclist-p set)
                             (vl-luciddb-p db)
                             (booleanp genp))))
 (let ((__function__ 'vl-lucid-dissect-var-main))
  (declare (ignorable __function__))
  (b*
   ((used (vl-lucidocclist-fix used))
    (set (vl-lucidocclist-fix set))
    (tag (tag item))
    (vartype
        (if (eq tag :vl-vardecl)
            (if (vl-scopestack-is-portdecl-p (vl-vardecl->name item)
                                             ss)
                "Port"
              "Variable")
          "Parameter"))
    (name (if (eq tag :vl-vardecl)
              (vl-vardecl->name item)
            (vl-paramdecl->name item)))
    (warnings (vl-lucid-multidrive-detect ss item set genp))
    ((when (and (atom used) (atom set)))
     (mv
      (warn :type (vl-lucid-warning-type :vl-lucid-spurious)
            :msg "~s0 ~w1 is never used or set anywhere. (~s2)"
            :args (list vartype name
                        (with-local-ps (vl-pp-scopestack-path ss))))
      nil))
    (used-solop (vl-lucid-some-solo-occp used))
    (set-solop (vl-lucid-some-solo-occp set))
    ((when (and used-solop set-solop))
     (mv warnings nil))
    ((mv simplep valid-bits)
     (vl-lucid-valid-bits-for-decl item ss))
    (warnings
     (b*
      (((when (atom used))
        (warn :type (vl-lucid-warning-type :vl-lucid-unused)
              :msg "~s0 ~w1 is set but is never used. (~s2)"
              :args (list vartype name
                          (with-local-ps (vl-pp-scopestack-path ss))
                          item)))
       ((when used-solop) warnings)
       ((unless (and simplep (vl-lucid-all-slices-p used)
                     (vl-lucid-all-slices-resolved-p used)))
        warnings)
       (used-bits (vl-lucid-resolved-slices->bits used item))
       (unused-bits (difference valid-bits used-bits))
       ((unless unused-bits) warnings))
      (warn
        :type (vl-lucid-warning-type :vl-lucid-unused)
        :msg "~s0 ~w1 has some bits that are never used: ~s2. (~s3)"
        :args (list vartype name
                    (vl-lucid-summarize-bits unused-bits)
                    (with-local-ps (vl-pp-scopestack-path ss))
                    item))))
    (warnings
     (b*
      (((when (atom set))
        (b*
         (((wmv just-passed-to-spurious-instances
                warnings)
           (vl-lucid-check-uses-are-spurious-instances
                name used db 100))
          ((when just-passed-to-spurious-instances)
           (warn
            :type :vl-lucid-spurious-port
            :msg
            "~s0 ~w1 is never set and is only passed to module instances where it is not used. (~s2)"
            :args (list vartype name
                        (with-local-ps (vl-pp-scopestack-path ss))
                        item))))
         (warn
              :type (vl-lucid-warning-type :vl-lucid-unset)
              :msg "~s0 ~w1 is used but is never initialized. (~s2)"
              :args (list vartype name
                          (with-local-ps (vl-pp-scopestack-path ss))
                          item))))
       ((when set-solop) warnings)
       ((unless (and simplep (vl-lucid-all-slices-p set)
                     (vl-lucid-all-slices-resolved-p set)))
        warnings)
       (set-bits (vl-lucid-resolved-slices->bits set item))
       (unset-bits (difference valid-bits set-bits))
       ((unless unset-bits) warnings))
      (warn
         :type (vl-lucid-warning-type :vl-lucid-unset)
         :msg "~s0 ~w1 has some bits that are never set: ~s2. (~s3)"
         :args (list vartype name
                     (vl-lucid-summarize-bits unset-bits)
                     (with-local-ps (vl-pp-scopestack-path ss))
                     item))))
    (typop (and (or (atom used) (atom set))
                (eq (tag item) :vl-vardecl)
                (consp (assoc-equal "VL_IMPLICIT"
                                    (vl-vardecl->atts item))))))
   (mv warnings typop))))

Theorem: vl-warninglist-p-of-vl-lucid-dissect-var-main.warnings

(defthm vl-warninglist-p-of-vl-lucid-dissect-var-main.warnings
  (b* (((mv ?warnings ?possible-typop)
        (vl-lucid-dissect-var-main ss item used set db genp)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: booleanp-of-vl-lucid-dissect-var-main.possible-typop

(defthm booleanp-of-vl-lucid-dissect-var-main.possible-typop
  (b* (((mv ?warnings ?possible-typop)
        (vl-lucid-dissect-var-main ss item used set db genp)))
    (booleanp possible-typop))
  :rule-classes :type-prescription)

Theorem: vl-lucid-dissect-var-main-of-vl-scopestack-fix-ss

(defthm vl-lucid-dissect-var-main-of-vl-scopestack-fix-ss
  (equal (vl-lucid-dissect-var-main (vl-scopestack-fix ss)
                                    item used set db genp)
         (vl-lucid-dissect-var-main ss item used set db genp)))

Theorem: vl-lucid-dissect-var-main-vl-scopestack-equiv-congruence-on-ss

(defthm
     vl-lucid-dissect-var-main-vl-scopestack-equiv-congruence-on-ss
 (implies
   (vl-scopestack-equiv ss ss-equiv)
   (equal
        (vl-lucid-dissect-var-main ss item used set db genp)
        (vl-lucid-dissect-var-main ss-equiv item used set db genp)))
 :rule-classes :congruence)

Theorem: vl-lucid-dissect-var-main-of-vl-lucidocclist-fix-used

(defthm vl-lucid-dissect-var-main-of-vl-lucidocclist-fix-used
  (equal
       (vl-lucid-dissect-var-main ss item (vl-lucidocclist-fix used)
                                  set db genp)
       (vl-lucid-dissect-var-main ss item used set db genp)))

Theorem: vl-lucid-dissect-var-main-vl-lucidocclist-equiv-congruence-on-used

(defthm
 vl-lucid-dissect-var-main-vl-lucidocclist-equiv-congruence-on-used
 (implies
   (vl-lucidocclist-equiv used used-equiv)
   (equal
        (vl-lucid-dissect-var-main ss item used set db genp)
        (vl-lucid-dissect-var-main ss item used-equiv set db genp)))
 :rule-classes :congruence)

Theorem: vl-lucid-dissect-var-main-of-vl-lucidocclist-fix-set

(defthm vl-lucid-dissect-var-main-of-vl-lucidocclist-fix-set
 (equal
   (vl-lucid-dissect-var-main ss item used (vl-lucidocclist-fix set)
                              db genp)
   (vl-lucid-dissect-var-main ss item used set db genp)))

Theorem: vl-lucid-dissect-var-main-vl-lucidocclist-equiv-congruence-on-set

(defthm
  vl-lucid-dissect-var-main-vl-lucidocclist-equiv-congruence-on-set
 (implies
   (vl-lucidocclist-equiv set set-equiv)
   (equal
        (vl-lucid-dissect-var-main ss item used set db genp)
        (vl-lucid-dissect-var-main ss item used set-equiv db genp)))
 :rule-classes :congruence)

Theorem: vl-lucid-dissect-var-main-of-vl-luciddb-fix-db

(defthm vl-lucid-dissect-var-main-of-vl-luciddb-fix-db
 (equal
     (vl-lucid-dissect-var-main ss item used set (vl-luciddb-fix db)
                                genp)
     (vl-lucid-dissect-var-main ss item used set db genp)))

Theorem: vl-lucid-dissect-var-main-vl-luciddb-equiv-congruence-on-db

(defthm vl-lucid-dissect-var-main-vl-luciddb-equiv-congruence-on-db
 (implies
   (vl-luciddb-equiv db db-equiv)
   (equal
        (vl-lucid-dissect-var-main ss item used set db genp)
        (vl-lucid-dissect-var-main ss item used set db-equiv genp)))
 :rule-classes :congruence)

Theorem: vl-lucid-dissect-var-main-of-bool-fix-genp

(defthm vl-lucid-dissect-var-main-of-bool-fix-genp
 (equal
  (vl-lucid-dissect-var-main ss
                             item used set db (acl2::bool-fix genp))
  (vl-lucid-dissect-var-main ss item used set db genp)))

Theorem: vl-lucid-dissect-var-main-iff-congruence-on-genp

(defthm vl-lucid-dissect-var-main-iff-congruence-on-genp
 (implies
   (iff genp genp-equiv)
   (equal
        (vl-lucid-dissect-var-main ss item used set db genp)
        (vl-lucid-dissect-var-main ss item used set db genp-equiv)))
 :rule-classes :congruence)