• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
        • Syntax
        • Loader
          • Preprocessor
            • Vl-iframe
            • Preprocessor-ifdef-minutia
            • Vl-preprocess
            • Vl-preprocess-loop
            • Vl-includeskips
              • Vl-includeskips-p
              • Vl-includeskips-fix
              • Vl-iskipinfo
              • Vl-match-proper-header-file-start-2
              • Vl-match-proper-header-file-start-1
              • Vl-multiple-include-begin
              • Vl-includeskips-equiv
              • Vl-includeskips-record-miss
              • Vl-includeskips-install-controller
              • Vl-includeskips-record-hit
              • Vl-skip-whitespace/comments
            • Vl-read-until-end-of-define
            • Vl-define-formallist->defaults
            • Vl-define
            • Vl-expand-define
            • Vl-read-include
            • Vl-substitute-into-macro-text
            • Vl-process-ifdef
            • Ppst
            • Vl-read-define-default-text
            • Vl-process-define
            • Preprocessor-include-minutia
            • Vl-trim-for-preproc
            • Vl-line-up-define-formals-and-actuals
            • Vl-process-undef
            • Vl-split-define-text
            • Vl-def-context
            • Vl-process-endif
            • Scan-backward-for-non-whitespace
            • Vl-ifdef-context
            • Scan-backward-for-whitespace
            • Vl-atvl-atts-text
            • Scan-for-non-whitespace
            • Vl-check-remaining-formals-all-have-defaults
            • Vl-process-else
            • Vl-is-compiler-directive-p
            • Vl-includeskips-controller-lookup
            • Vl-ifdef-use-map
            • Vl-defines
            • Vl-def-use-map
            • Vl-nice-bytes
            • Vl-safe-previous-n
            • Vl-safe-next-n
            • Vl-ppst-pad
            • Vl-filename-to-string-literal
            • Vl-maybe-update-filemap
            • *vl-preprocess-clock*
            • Vl-ppst->warnings
            • Vl-ppst->iskips
            • Vl-ppst->ifdefmap
            • Vl-ppst->idcache
            • Vl-istack
            • Vl-ppst->istack
            • Vl-ppst->includes
            • Vl-ppst->filemap
            • Vl-ppst->defmap
            • Vl-ppst->defines
            • Vl-ppst->config
            • Vl-ppst->bytes
            • Vl-ppst->activep
            • Vl-ppst->acc
            • Vl-ppst-record-ifdef-use
            • Vl-ppst-record-def-use
            • Vl-ifdef-context-list
            • Vl-def-context-list
            • Vl-ppst-update-warnings
            • Vl-ppst-update-istack
            • Vl-ppst-update-iskips
            • Vl-ppst-update-includes
            • Vl-ppst-update-ifdefmap
            • Vl-ppst-update-idcache
            • Vl-ppst-update-filemap
            • Vl-ppst-update-defmap
            • Vl-ppst-update-defines
            • Vl-ppst-update-config
            • Vl-ppst-update-activep
            • Vl-ppst-update-bytes
            • Vl-ppst-update-acc
            • Vl-ppst-unsound-nreverse-acc
          • Vl-loadconfig
          • Vl-loadstate
          • Lexer
          • Parser
          • Vl-load-merge-descriptions
          • Vl-find-basename/extension
          • Vl-load-file
          • Vl-loadresult
          • Scope-of-defines
          • Vl-find-file
          • Vl-flush-out-descriptions
          • Vl-description
          • Vl-read-file
          • Vl-includeskips-report-gather
          • Vl-load-main
          • Extended-characters
          • Vl-load
          • Vl-load-description
          • Vl-descriptions-left-to-load
          • Inject-warnings
          • Vl-preprocess-debug
          • Vl-write-preprocessor-debug-file
          • Vl-read-file-report-gather
          • Vl-load-descriptions
          • Vl-load-files
          • Translate-off
          • Vl-load-read-file-hook
          • Vl-read-file-report
          • Vl-loadstate-pad
          • Vl-load-summary
          • Vl-collect-modules-from-descriptions
          • Vl-loadstate->warnings
          • Vl-iskips-report
          • Vl-descriptionlist
        • Warnings
        • Getting-started
        • Utilities
        • Printer
        • Kit
        • Mlib
        • Transforms
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Preprocessor

Vl-includeskips

A record of which files we have already included that have ``proper'' include guards and may not need to be included again.

Header files often have the form

`ifndef included_foo
`define included_foo
   ...
`endif

Or equivalently (and possibly common in legacy code since historically ifndef wasn't supported by some tools):

`ifdef included_foo
`else
   `define included_foo
   ...
`endif

In the typical case where included_foo never gets undefined, it is good for performance to completely skip subsequent includes of such files.

To accomplish this, we maintain an includeskips alist, which is a (fast) alist binding pathnames of files that we have `included so far to vl-iskipinfos that contain the names of their controlling define, e.g., included_foo (and some additional information).

These controlling defines should only be added to the includeskips when we determine that they have the proper form. Later, when we encounter a new `include, we can check whether the file is in the includeskips and, if so, whether its controlling define is still `defined. If so, we can avoid the pointless work of re-opening the file, re-reading its characters, and re-preprocessing them, because we know that after expanding the ifdefs, the file will make no contribution to the post-preprocessed text we are building.

To identify files that match the proper form, when we open a file due to an `include, we check whether the file begins with one of the above, ``proper'' include-guard formats; see vl-multiple-include-begin. This identification is pretty efficient: we only have to scan initial comments, whitespace, and a few tokens. If we find a proper include-guard start, we push a special vl-iframe, corresponding to the ifndef included_foo. This iframe is marked as multiple-include candidate whose controller is included_foo. We then skip until just before the `define and resume preprocessing.

We have to be careful, as we process the body of the included file, to be sure to remove this marking if we ever encounter an `else or `elseif that's part of the special top-level `ifndef. This is done in vl-process-ifdef and vl-process-else.

When we finally get to the `endif, we notice in vl-process-endif that we have a special frame. If so, we know that (1) the start of the file begins with a suitable ifndef/define pair and (2) there have been no `else or `elseif directives attached with this pair along the way. So, the only thing left to check is that the remainder of the file consists of nothing but whitespace and comments, which is easy and efficient. If so, we're set: the file has the desired form, so we add it to the includeskips alist.

Subtopics

Vl-includeskips-p
Recognizer for vl-includeskips.
Vl-includeskips-fix
(vl-includeskips-fix x) is an fty alist fixing function that follows the fix-keys strategy.
Vl-iskipinfo
Information about the multiple-include status of an individual file.
Vl-match-proper-header-file-start-2
Match the start of a ``proper'' ifdef-controlled header file.
Vl-match-proper-header-file-start-1
Match the start of a ``proper'' ifndef-controlled header file.
Vl-multiple-include-begin
Check a file for a proper include-guard header; if so, install a special iframe and skip past the initial ifndef part, otherwise leave the file alone.
Vl-includeskips-equiv
Basic equivalence relation for vl-includeskips structures.
Vl-includeskips-record-miss
Record that a file is not being skipped due to multiple include optimization.
Vl-includeskips-install-controller
Install the controlling define into the vl-includeskips. This should be done when the final `endif is encountered and determined to be ok.
Vl-includeskips-record-hit
Record that a file is being successfully skipped due to multiple include optimization.
Vl-skip-whitespace/comments
For use in vl-includeskips, just skip past any whitespace and comments.