• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
      • Syntax
      • Loader
      • Warnings
        • Lint-warning-suppression
        • Warning-basics
        • Vl-warning
        • Vl-warninglist-add-ctx
        • Vl-warninglist->types
        • Propagating-errors
        • Vl-reportcard
          • Vl-reportcard-p
          • Vl-apply-reportcard
          • Vl-reportcard-fix
          • Vl-extend-reportcard-list
          • Vl-design-reportcard
          • Vl-design-origname-reportcard
          • Vl-extend-reportcard
          • Vl-reportcard-revive-invalid-warnings
          • Vl-clean-reportcard
          • Vl-remove-from-reportcard
          • Vl-reportcard-equiv
          • Vl-print-reportcard
            • Vl-elide-warnings
              • Vl-elide-warnings-main
            • Vl-print-reportcard-aux
          • Vl-keep-from-reportcard
          • Vl-reportcard-to-string
          • Vl-reportcard-types
          • Vl-reportcardkey-p
        • Vl-some-warning-fatalp
        • Clean-warnings
        • Lint-whole-file-suppression
        • Warn
        • Vl-warninglist
        • Vl-remove-warnings
        • Vl-keep-warnings
        • Flat-warnings
        • Vl-some-warning-of-type-p
        • Vl-msg
        • Vl-warning-add-ctx
        • Vl-print-warning
        • Vmsg-binary-concat
        • Ok
        • Vl-trace-warnings
        • Fatal
        • Vmsg
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-elide-warnings

Vl-elide-warnings-main

Signature

(vl-elide-warnings-main x cutoff suppressed counts-fal acc) 
  → 
(mv acc counts-fal suppressed)

Arguments

x — Guard (vl-warninglist-p x).

cutoff — Max number of warnings of a single type to keep.
    Guard (natp cutoff).

suppressed — Types of warnings, with duplicates, that we have suppressed so far.
    Guard (symbol-listp suppressed).

counts-fal — Fast alist, binds type -> count, where count is how many warnings of this type have been seen so far.

acc — Guard (vl-warninglist-p acc).

Returns

acc — Type (vl-warninglist-p acc).

suppressed — Type (symbol-listp suppressed).

Definitions and Theorems

Function: vl-elide-warnings-main

(defun vl-elide-warnings-main (x cutoff suppressed counts-fal acc)
  (declare (xargs :guard (and (vl-warninglist-p x)
                              (natp cutoff)
                              (symbol-listp suppressed)
                              (vl-warninglist-p acc))))
  (let ((__function__ 'vl-elide-warnings-main))
    (declare (ignorable __function__))
    (b* ((x (vl-warninglist-fix x))
         (acc (vl-warninglist-fix acc))
         (cutoff (lnfix cutoff))
         ((when (atom x))
          (mv acc cutoff
              (acl2::symbol-list-fix suppressed)))
         ((vl-warning x1) (car x))
         (curr (nfix (cdr (hons-get x1.type counts-fal))))
         (counts-fal (hons-acons x1.type (+ 1 curr)
                                 counts-fal))
         (keep-p (< curr cutoff))
         (acc (if keep-p (cons x1 acc) acc))
         (suppressed (if keep-p suppressed
                       (cons x1.type
                             (acl2::symbol-list-fix suppressed)))))
      (vl-elide-warnings-main (cdr x)
                              cutoff suppressed counts-fal acc))))

Theorem: vl-warninglist-p-of-vl-elide-warnings-main.acc

(defthm vl-warninglist-p-of-vl-elide-warnings-main.acc
 (b* (((mv ?acc ?counts-fal ?suppressed)
       (vl-elide-warnings-main x cutoff suppressed counts-fal acc)))
   (vl-warninglist-p acc))
 :rule-classes :rewrite)

Theorem: symbol-listp-of-vl-elide-warnings-main.suppressed

(defthm symbol-listp-of-vl-elide-warnings-main.suppressed
 (b* (((mv ?acc ?counts-fal ?suppressed)
       (vl-elide-warnings-main x cutoff suppressed counts-fal acc)))
   (symbol-listp suppressed))
 :rule-classes :rewrite)

Theorem: vl-elide-warnings-main-of-vl-warninglist-fix-x

(defthm vl-elide-warnings-main-of-vl-warninglist-fix-x
  (equal
       (vl-elide-warnings-main (vl-warninglist-fix x)
                               cutoff suppressed counts-fal acc)
       (vl-elide-warnings-main x cutoff suppressed counts-fal acc)))

Theorem: vl-elide-warnings-main-vl-warninglist-equiv-congruence-on-x

(defthm vl-elide-warnings-main-vl-warninglist-equiv-congruence-on-x
 (implies
  (vl-warninglist-equiv x x-equiv)
  (equal (vl-elide-warnings-main x cutoff suppressed counts-fal acc)
         (vl-elide-warnings-main x-equiv
                                 cutoff suppressed counts-fal acc)))
 :rule-classes :congruence)

Theorem: vl-elide-warnings-main-of-nfix-cutoff

(defthm vl-elide-warnings-main-of-nfix-cutoff
  (equal
       (vl-elide-warnings-main x (nfix cutoff)
                               suppressed counts-fal acc)
       (vl-elide-warnings-main x cutoff suppressed counts-fal acc)))

Theorem: vl-elide-warnings-main-nat-equiv-congruence-on-cutoff

(defthm vl-elide-warnings-main-nat-equiv-congruence-on-cutoff
 (implies
  (acl2::nat-equiv cutoff cutoff-equiv)
  (equal (vl-elide-warnings-main x cutoff suppressed counts-fal acc)
         (vl-elide-warnings-main x cutoff-equiv
                                 suppressed counts-fal acc)))
 :rule-classes :congruence)

Theorem: vl-elide-warnings-main-of-symbol-list-fix-suppressed

(defthm vl-elide-warnings-main-of-symbol-list-fix-suppressed
  (equal
       (vl-elide-warnings-main x cutoff
                               (acl2::symbol-list-fix suppressed)
                               counts-fal acc)
       (vl-elide-warnings-main x cutoff suppressed counts-fal acc)))

Theorem: vl-elide-warnings-main-symbol-list-equiv-congruence-on-suppressed

(defthm
  vl-elide-warnings-main-symbol-list-equiv-congruence-on-suppressed
 (implies
  (acl2::symbol-list-equiv suppressed suppressed-equiv)
  (equal (vl-elide-warnings-main x cutoff suppressed counts-fal acc)
         (vl-elide-warnings-main x cutoff
                                 suppressed-equiv counts-fal acc)))
 :rule-classes :congruence)

Theorem: vl-elide-warnings-main-of-vl-warninglist-fix-acc

(defthm vl-elide-warnings-main-of-vl-warninglist-fix-acc
  (equal
       (vl-elide-warnings-main x cutoff suppressed
                               counts-fal (vl-warninglist-fix acc))
       (vl-elide-warnings-main x cutoff suppressed counts-fal acc)))

Theorem: vl-elide-warnings-main-vl-warninglist-equiv-congruence-on-acc

(defthm
      vl-elide-warnings-main-vl-warninglist-equiv-congruence-on-acc
 (implies
  (vl-warninglist-equiv acc acc-equiv)
  (equal (vl-elide-warnings-main x cutoff suppressed counts-fal acc)
         (vl-elide-warnings-main x cutoff
                                 suppressed counts-fal acc-equiv)))
 :rule-classes :congruence)