• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
        • Vl-warninglist->types
        • Vl-warning
        • Propagating-errors
        • Vl-reportcard
        • Vl-warning-sort
          • Vl-warning-<
        • Lint-warning-suppression
        • Clean-warnings
        • Warn
        • Vl-some-warning-fatalp
        • Vl-print-warnings-with-header
        • Vl-print-warnings-with-named-header
        • Flat-warnings
        • Vl-keep-warnings
        • Vl-remove-warnings
        • Vl-print-warnings
        • Vl-some-warning-of-type-p
        • Vl-clean-warnings
        • Vl-warnings-to-string
        • Vl-warninglist
        • Vl-print-warning
        • Ok
        • Vl-trace-warnings
        • Fatal
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Warnings

Vl-warning-sort

Mergesort warnings using vl-warning-<

Definitions and Theorems

Function: vl-warning-list-p

(defun vl-warning-list-p (acl2::x)
       (declare (xargs :guard t :stobjs nil))
       (if (consp acl2::x)
           (and (vl-warning-p (car acl2::x))
                (vl-warning-list-p (cdr acl2::x)))
           t))

Function: vl-warning-ordered-p

(defun vl-warning-ordered-p (acl2::x)
       (declare (xargs :guard (and t (vl-warning-list-p acl2::x))
                       :stobjs nil))
       (cond ((atom acl2::x) t)
             ((atom (cdr acl2::x)) t)
             ((vl-warning-< (first acl2::x)
                            (second acl2::x))
              (vl-warning-ordered-p (cdr acl2::x)))
             (t (and (not (vl-warning-< (second acl2::x)
                                        (first acl2::x)))
                     (vl-warning-ordered-p (cdr acl2::x))))))

Function: vl-warning-merge

(defun vl-warning-merge (acl2::x acl2::y)
       (declare (xargs :stobjs nil
                       :guard (and t (vl-warning-list-p acl2::x)
                                   (vl-warning-list-p acl2::y))))
       (cond ((atom acl2::x) acl2::y)
             ((atom acl2::y) acl2::x)
             ((vl-warning-< (car acl2::y)
                            (car acl2::x))
              (cons (car acl2::y)
                    (vl-warning-merge acl2::x (cdr acl2::y))))
             (t (cons (car acl2::x)
                      (vl-warning-merge (cdr acl2::x)
                                        acl2::y)))))

Function: vl-warning-merge-tr

(defun
    vl-warning-merge-tr
    (acl2::x acl2::y acl2::acc)
    (declare (xargs :stobjs nil
                    :guard (and t (vl-warning-list-p acl2::x)
                                (vl-warning-list-p acl2::y))))
    (cond ((atom acl2::x)
           (revappend-without-guard acl2::acc acl2::y))
          ((atom acl2::y)
           (revappend-without-guard acl2::acc acl2::x))
          ((vl-warning-< (car acl2::y)
                         (car acl2::x))
           (vl-warning-merge-tr acl2::x (cdr acl2::y)
                                (cons (car acl2::y) acl2::acc)))
          (t (vl-warning-merge-tr (cdr acl2::x)
                                  acl2::y
                                  (cons (car acl2::x) acl2::acc)))))

Function: vl-warning-mergesort-fixnum

(defun
 vl-warning-mergesort-fixnum
 (acl2::x len)
 (declare (xargs :stobjs nil
                 :guard (and t (vl-warning-list-p acl2::x)
                             (natp len)
                             (<= len (len acl2::x))))
          (type (signed-byte 30) len))
 (cond
  ((mbe :logic (zp len)
        :exec (eql (the (signed-byte 30) len) 0))
   nil)
  ((eql (the (signed-byte 30) len) 1)
   (list (car acl2::x)))
  (t
   (let*
     ((acl2::len1 (the (signed-byte 30)
                       (ash (the (signed-byte 30) len) -1)))
      (acl2::len2 (the (signed-byte 30)
                       (- (the (signed-byte 30) len)
                          (the (signed-byte 30) acl2::len1))))
      (acl2::part1 (vl-warning-mergesort-fixnum acl2::x acl2::len1))
      (acl2::part2
           (vl-warning-mergesort-fixnum (rest-n acl2::len1 acl2::x)
                                        acl2::len2)))
     (vl-warning-merge-tr acl2::part1 acl2::part2 nil)))))

Function: vl-warning-mergesort-integers

(defun
 vl-warning-mergesort-integers
 (acl2::x len)
 (declare (xargs :stobjs nil
                 :guard (and t (vl-warning-list-p acl2::x)
                             (natp len)
                             (<= len (len acl2::x))))
          (type integer len))
 (cond
  ((mbe :logic (zp len)
        :exec (eql (the integer len) 0))
   nil)
  ((eql (the integer len) 1)
   (list (car acl2::x)))
  (t
   (let*
    ((acl2::len1 (the integer (ash (the integer len) -1)))
     (acl2::len2 (the integer
                      (- (the integer len)
                         (the integer acl2::len1))))
     (acl2::part1
          (if (< (the integer acl2::len1)
                 (acl2::mergesort-fixnum-threshold))
              (vl-warning-mergesort-fixnum acl2::x acl2::len1)
              (vl-warning-mergesort-integers acl2::x acl2::len1)))
     (acl2::part2
      (if (< (the integer acl2::len2)
             (acl2::mergesort-fixnum-threshold))
          (vl-warning-mergesort-fixnum (rest-n acl2::len1 acl2::x)
                                       acl2::len2)
          (vl-warning-mergesort-integers (rest-n acl2::len1 acl2::x)
                                         acl2::len2))))
    (vl-warning-merge-tr acl2::part1 acl2::part2 nil)))))

Function: vl-warning-sort

(defun
 vl-warning-sort (acl2::x)
 (declare (xargs :guard (and t (vl-warning-list-p acl2::x))
                 :stobjs nil))
 (mbe
  :logic
  (cond
      ((atom acl2::x) nil)
      ((atom (cdr acl2::x))
       (list (car acl2::x)))
      (t (let ((acl2::half (floor (len acl2::x) 2)))
              (vl-warning-merge
                   (vl-warning-sort (take acl2::half acl2::x))
                   (vl-warning-sort (nthcdr acl2::half acl2::x))))))
  :exec (let ((len (len acl2::x)))
             (if (< len (acl2::mergesort-fixnum-threshold))
                 (vl-warning-mergesort-fixnum acl2::x len)
                 (vl-warning-mergesort-integers acl2::x len)))))

Theorem: vl-warning-sort-preserves-duplicity

(defthm vl-warning-sort-preserves-duplicity
        (equal (duplicity acl2::a (vl-warning-sort acl2::x))
               (duplicity acl2::a acl2::x)))

Theorem: vl-warning-sort-creates-comparable-listp

(defthm vl-warning-sort-creates-comparable-listp
        (implies (vl-warning-list-p acl2::x)
                 (vl-warning-list-p (vl-warning-sort acl2::x))))

Theorem: vl-warning-sort-sorts

(defthm vl-warning-sort-sorts
        (vl-warning-ordered-p (vl-warning-sort acl2::x)))

Theorem: vl-warning-sort-no-duplicatesp-equal

(defthm vl-warning-sort-no-duplicatesp-equal
        (equal (no-duplicatesp-equal (vl-warning-sort acl2::x))
               (no-duplicatesp-equal acl2::x)))

Theorem: vl-warning-sort-true-listp

(defthm vl-warning-sort-true-listp
        (true-listp (vl-warning-sort acl2::x))
        :rule-classes :type-prescription)

Theorem: vl-warning-sort-len

(defthm vl-warning-sort-len
        (equal (len (vl-warning-sort acl2::x))
               (len acl2::x)))

Theorem: vl-warning-sort-consp

(defthm vl-warning-sort-consp
        (equal (consp (vl-warning-sort acl2::x))
               (consp acl2::x)))

Theorem: vl-warning-sort-is-identity-under-set-equiv

(defthm vl-warning-sort-is-identity-under-set-equiv
        (set-equiv (vl-warning-sort acl2::x)
                   acl2::x))

Theorem: vl-warning-list-p-is-vl-warninglist-p

(defthm vl-warning-list-p-is-vl-warninglist-p
        (equal (vl-warning-list-p x)
               (vl-warninglist-p x)))

Theorem: vl-warninglist-p-of-vl-warning-sort

(defthm vl-warninglist-p-of-vl-warning-sort
        (implies (force (vl-warninglist-p x))
                 (vl-warninglist-p (vl-warning-sort x))))

Theorem: consp-of-vl-warning-sort

(defthm consp-of-vl-warning-sort
        (equal (consp (vl-warning-sort x))
               (consp x)))

Subtopics

Vl-warning-<

A basic, rather arbitrary ordering for warnings.