		Search-engine friendly clone of the ACL2 documentation.

Vl-commentmap-p

Vl-adjust-minloc-for-comments

Tweak starting location so that we get comments preceding the module keyword.

Signature
(vl-adjust-minloc-for-comments acc minloc descs) → adjusted-minloc
Arguments: acc — Initially line 0 of the file.
Guard (vl-location-p acc).; minloc — True minloc of the module we're considering.
Guard (vl-location-p minloc).; descs — All top-level descriptions found in the file.
Guard (vl-descriptionlist-p descs).
Returns: adjusted-minloc — Type (vl-location-p adjusted-minloc), given the guard.

It turns out that useful comments about a module (or other kind of top-level description) are often put before the module instead of within it. For instance:

// Module: SuchAndSo
// Author: John Q. Designer
// Purpose: This module is responsible for blah blah blah.  It
//          interfaces with units blah and blah, and implements ...
// ...
module SuchAndSo (...) ;
  ...
endmodule

This is especially common when modules are written in separate files, and the comments describing the module are found at the top. Unfortunately, our basic approach to comment gathering—associating all comments between module and endmodule—misses these comments.

To correct for this, we no longer use the actual minloc for the module. Instead, we (almost) choose the largest maxloc of any other module such that other-maxloc < minloc. That sounds like gibberish but it makes sense if you just draw what portion of the file you want:

module foo1 (...);
 ...
endmodule

module foo2 (...);
 ...
endmodule              <-- largest maxloc less than minloc of bar

// helpful comments about module bar, which we
// want to make sure are associated with bar.
module bar (...);
 ...
endmodule

Well, we don't quite use the maxloc of the previous module. Instead, we use maxloc+1. The reason for this is that sometimes people put in really stupid comments after end keywords, such as:

module foo (...);
  ...
endmodule // foo

And we don't want to associate this // foo comment with the subsequent module.

Definitions and Theorems

Function: vl-adjust-minloc-for-comments

(defun vl-adjust-minloc-for-comments (acc minloc descs)
  (declare (xargs :guard (and (vl-location-p acc)
                              (vl-location-p minloc)
                              (vl-descriptionlist-p descs))))
  (let ((__function__ 'vl-adjust-minloc-for-comments))
    (declare (ignorable __function__))
    (b* (((when (atom descs)) acc)
         (mod1.maxloc (vl-description->maxloc (car descs)))
         ((unless (and (equal (vl-location->filename acc)
                              (vl-location->filename mod1.maxloc))
                       (< (vl-location->line mod1.maxloc)
                          (vl-location->line minloc))
                       (< (vl-location->line acc)
                          (vl-location->line mod1.maxloc))))
          (vl-adjust-minloc-for-comments acc minloc (cdr descs)))
         (acc (change-vl-location
                   acc
                   :line (min (+ 1 (vl-location->line mod1.maxloc))
                              (vl-location->line minloc)))))
      (vl-adjust-minloc-for-comments acc minloc (cdr descs)))))

Theorem: vl-location-p-of-vl-adjust-minloc-for-comments

(defthm vl-location-p-of-vl-adjust-minloc-for-comments
  (implies
       (and (vl-location-p$inline acc)
            (vl-location-p$inline minloc)
            (vl-descriptionlist-p descs))
       (b* ((adjusted-minloc
                 (vl-adjust-minloc-for-comments acc minloc descs)))
         (vl-location-p adjusted-minloc)))
  :rule-classes :rewrite)

Theorem: bound-of-vl-adjust-minloc-for-comments

(defthm bound-of-vl-adjust-minloc-for-comments
 (implies (and (<= (vl-location->line acc)
                   (vl-location->line minloc))
               (force (vl-location-p acc))
               (force (vl-location-p minloc))
               (force (vl-descriptionlist-p descs)))
          (<= (vl-location->line
                   (vl-adjust-minloc-for-comments acc minloc descs))
              (vl-location->line minloc)))
 :rule-classes ((:rewrite) (:linear)))