• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vl
        • Syntax
        • Loader
          • Preprocessor
          • Vl-loadconfig
          • Vl-loadstate
            • Vl-loadstate-p
            • Vl-loadstate-fix
            • Make-vl-loadstate
            • Vl-loadstate-equiv
            • Vl-loadstate->descalist
            • Vl-loadstate->descs
            • Change-vl-loadstate
            • Vl-loadstate->reportcard
            • Vl-loadstate-warn
            • Vl-loadstate->spcache
            • Vl-loadstate->pstate
            • Vl-loadstate->iskips
            • Vl-loadstate->ifdefmap
            • Vl-loadstate->idcache
            • Vl-loadstate->filemap
            • Vl-loadstate->defmap
            • Vl-loadstate->defines
            • Vl-loadstate->config
            • Vl-loadstate-fatal
            • Vl-loadstate->bytes
            • Vl-loadstate-set-warnings
          • Lexer
          • Parser
          • Vl-load-merge-descriptions
          • Vl-find-basename/extension
          • Vl-load-file
          • Vl-loadresult
          • Vl-find-file
          • Scope-of-defines
          • Vl-flush-out-descriptions
          • Vl-description
          • Vl-read-file
          • Vl-includeskips-report-gather
          • Vl-load-main
          • Extended-characters
          • Vl-load
          • Vl-load-description
          • Vl-preprocess-debug
          • Vl-descriptions-left-to-load
          • Inject-warnings
          • Vl-read-file-report-gather
          • Vl-write-preprocessor-debug-file
          • Vl-load-descriptions
          • Vl-load-files
          • Translate-off
          • Vl-load-read-file-hook
          • Vl-loadstate-pad
          • Vl-read-file-report
          • 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
    • Testing-utilities
    • Math
  • Loader

Vl-loadstate

Internal state object used throughout the VL loading routines.

This is a product type introduced by defprod.

Fields
config — vl-loadconfig
Original configuration passed to vl-load. This remains constant throughout our loading routines.
descs — vl-descriptionlist
Top-level descriptions (modules, packages, interfaces, etc.) we have loaded so far. These descriptions have been only minimally transformed, and are intended to capture the actual source code in the files on disk. These are always kept in the reverse order that they are encountered (i.e., accumulator style), which is important for lexical scoping.
descalist
Fast alist of description names, for fast lookups.
defines — vl-defines
The current set of `defines at any point in time.
iskips — vl-includeskips
Supports multiple-include optimization in the preprocessor.
ifdefmap — vl-ifdef-use-map
Log of which `defines are used by `ifdefs.
defmap — vl-def-use-map
Log of which `defines are used by non-`ifdefs.
idcache — vl-dirlist-cache
Cache for the contents of the :include-dirs.
spcache — vl-dirxlist-cache
Cache for the contents of the :search-path.
reportcard — vl-reportcard
Main storage for load-time warnings that we want to associate with particular descriptions. This is where most load-time warnings from loading are kept during loading. At the end of loading, these warnings get injected into the actual descriptions they pertain to.
pstate — vl-parsestate
State that the parser needs. BOZO probably we should consider moving some of the loadstate into the pstate. This holds, among other things, any "floating" warnings that aren't associated with any description. But few warnings get put here. Instead, most warnings get associated with particular descriptions. But some warnings from the early stages of file loading (like preprocessing and lexing), or warnings about malformed syntax that occurs between descriptions, can end up here.
filemap — vl-filemap
Database mapping the names of files we have read to their contents. This is occasionally useful for seeing the original code for a description. To save memory, you can avoid constructing this alist; see the filemapp option in vl-loadconfig-p.
bytes — natp
Total bytes of input files read so far.
Additional Requirements

The following invariant is enforced on the fields:

(equal descalist (vl-make-descalist descs))

Subtopics

Vl-loadstate-p
Recognizer for vl-loadstate structures.
Vl-loadstate-fix
Fixing function for vl-loadstate structures.
Make-vl-loadstate
Basic constructor macro for vl-loadstate structures.
Vl-loadstate-equiv
Basic equivalence relation for vl-loadstate structures.
Vl-loadstate->descalist
Get the descalist field from a vl-loadstate.
Vl-loadstate->descs
Get the descs field from a vl-loadstate.
Change-vl-loadstate
Modifying constructor for vl-loadstate structures.
Vl-loadstate->reportcard
Get the reportcard field from a vl-loadstate.
Vl-loadstate-warn
Vl-loadstate->spcache
Get the spcache field from a vl-loadstate.
Vl-loadstate->pstate
Get the pstate field from a vl-loadstate.
Vl-loadstate->iskips
Get the iskips field from a vl-loadstate.
Vl-loadstate->ifdefmap
Get the ifdefmap field from a vl-loadstate.
Vl-loadstate->idcache
Get the idcache field from a vl-loadstate.
Vl-loadstate->filemap
Get the filemap field from a vl-loadstate.
Vl-loadstate->defmap
Get the defmap field from a vl-loadstate.
Vl-loadstate->defines
Get the defines field from a vl-loadstate.
Vl-loadstate->config
Get the config field from a vl-loadstate.
Vl-loadstate-fatal
Vl-loadstate->bytes
Get the bytes field from a vl-loadstate.
Vl-loadstate-set-warnings