• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
        • Preprocessor
        • Vl-loadconfig
        • Lexer
        • Vl-loadstate
        • Parser
        • Vl-load-merge-descriptions
        • Scope-of-defines
        • Vl-load-file
        • Vl-flush-out-descriptions
        • Vl-description
        • Vl-loadresult
        • Vl-read-file
        • Vl-find-basename/extension
        • Vl-read-files
        • Vl-find-file
        • Extended-characters
        • Vl-load
        • Vl-load-main
        • Vl-load-description
        • Vl-descriptions-left-to-load
        • Inject-warnings
        • Vl-load-descriptions
        • Vl-load-files
        • Vl-load-summary
        • Vl-collect-modules-from-descriptions
        • Vl-descriptionlist
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Loader

Vl-flush-out-descriptions

Attempt to find and load any missing modules.

Signature

(vl-flush-out-descriptions st n state) → (mv st state)

Arguments

st — Guard (vl-loadstate-p st).

n — Counter to force termination.
    Guard (natp n).

Returns

st — Type (vl-loadstate-p st).

state — Type (state-p1 state), given (force (state-p1 state)).

After some initial files have been loaded, it is generally necessary to track down and load, e.g., any submodules that have been referenced but not defined. We call this process "flushing out" the description list.

To find some description foo, we look through the provided search directories, in order, for a file whose name is foo.v. (We can also consider files with other extensions, see the search-exts option in vl-loadconfig-p.)

We try to load the first such foo.v that we find. This is not necessarily sensible. It might be, for instance, that foo.v will not define anything named foo, or that it will define all sorts of other modules instead of foo. In other words, for this search procedure to make sense, you need to follow a sort of naming discipline and keep descriptions in files that have appropriate names.

Flushing out the descriptions is necessarily an iterative process. After we load some library module foo, we might find that it references some other library module bar that we have not yet loaded. To ensure that the process will eventually terminate, so cap the maximum number of times we will look for new modules.

Definitions and Theorems

Function: vl-flush-out-descriptions

(defun
 vl-flush-out-descriptions (st n state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (vl-loadstate-p st) (natp n))))
 (let
  ((__function__ 'vl-flush-out-descriptions))
  (declare (ignorable __function__))
  (b*
   ((st (vl-loadstate-fix st))
    (missing (vl-descriptions-left-to-load st))
    ((unless missing) (mv st state))
    ((when (zp n))
     (mv
      (vl-loadstate-warn
       :type :vl-flush-failed
       :msg
       "Failed to load description~s0 ~&1 ~
                                     because we reached the maximum number of ~
                                     tries."
       :args (list (if (vl-plural-p missing) "s" "")
                   missing))
      state))
    (num-prev (len (vl-loadstate->descs st)))
    ((mv st state)
     (vl-load-descriptions missing st state))
    (num-new (len (vl-loadstate->descs st)))
    ((when (equal num-prev num-new))
     (mv (vl-loadstate-warn
              :type :vl-search-failed
              :msg "Failed to find ~x0 description~s1: ~&2."
              :args (list (length missing)
                          (if (vl-plural-p missing) "s" "")
                          (mergesort missing)))
         state)))
   (vl-flush-out-descriptions st (- n 1)
                              state))))

Theorem: vl-loadstate-p-of-vl-flush-out-descriptions.st

(defthm vl-loadstate-p-of-vl-flush-out-descriptions.st
        (b* (((mv ?st acl2::?state)
              (vl-flush-out-descriptions st n state)))
            (vl-loadstate-p st))
        :rule-classes :rewrite)

Theorem: state-p1-of-vl-flush-out-descriptions.state

(defthm state-p1-of-vl-flush-out-descriptions.state
        (implies (force (state-p1 state))
                 (b* (((mv ?st acl2::?state)
                       (vl-flush-out-descriptions st n state)))
                     (state-p1 state)))
        :rule-classes :rewrite)