		Search-engine friendly clone of the ACL2 documentation.

Loader

Vl-load-file

Main function for loading a single Verilog file.

Signature
(vl-load-file filename st state) → (mv st state)
Arguments: filename — Guard (stringp filename).; st — Guard (vl-loadstate-p st).
Returns: st — Type (vl-loadstate-p st).; state — Type (state-p1 state), given (force (state-p1 state)).

Even loading a single file is a multi-step process:

The contents of the file are loaded via vl-read-file into a list of extended-characters in memory.
The preprocessor then expands away compiler directives like `defines, producing a new list of extended characters.
The lexer converts the preprocessed character list into a list of tokens.
The parser transforms the token list into a list of descriptions.
We merge these newly loaded descriptions into the loader's state.

Definitions and Theorems

Function: vl-load-file

(defun vl-load-file (filename st state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (stringp filename)
                             (vl-loadstate-p st))))
 (let ((__function__ 'vl-load-file))
  (declare (ignorable __function__))
  (b*
   (((vl-loadstate st) st)
    ((vl-loadconfig st.config) st.config)
    (pad (vl-loadstate-pad st))
    (- (cw-unformatted (cat pad filename *nls*)))
    ((mv okp contents len state)
     (time$ (vl-read-file (string-fix filename))
            :msg "~s0 (read: ~st sec, ~sa bytes)~%"
            :args (list pad)
            :mintime st.config.mintime))
    ((unless okp)
     (mv (vl-loadstate-fatal :type :vl-read-failed
                             :msg "Error reading file ~s0."
                             :args (list filename)
                             :st st)
         state))
    (new-bytes (+ len st.bytes))
    (st (change-vl-loadstate st
                             :bytes new-bytes))
    (pad (vl-loadstate-pad st))
    (filemap
         (time$ (and st.config.filemapp
                     (cons (cons filename
                                 (vl-echarlist->string contents))
                           st.filemap))
                :msg "~s0 (filemap: ~st sec, ~sa bytes)~%"
                :args (list pad)
                :mintime st.config.mintime))
    ((mv successp
         defines filemap iskips ifdefmap defmap
         bytes warnings preprocessed state)
     (time$ (vl-preprocess contents
                           :defines st.defines
                           :filemap filemap
                           :iskips st.iskips
                           :ifdefmap st.ifdefmap
                           :defmap st.defmap
                           :bytes new-bytes
                           :config st.config
                           :idcache st.idcache
                           :warnings (vl-loadstate->warnings st))
            :msg "~s0 (preprocess: ~st sec, ~sa bytes)~%"
            :args (list pad)
            :mintime st.config.mintime))
    (st (vl-loadstate-set-warnings warnings))
    (st (change-vl-loadstate st
                             :iskips iskips
                             :ifdefmap ifdefmap
                             :defmap defmap
                             :bytes bytes))
    ((unless successp)
     (b* ((st (change-vl-loadstate
                   st
                   :defines (make-fast-alist st.defines))))
       (mv (vl-loadstate-fatal :type :vl-preprocess-failed
                               :msg "Preprocessing failed for ~s0."
                               :args (list filename)
                               :st st)
           state)))
    ((mv preprocessed state)
     (vl-preprocess-debug filename preprocessed st state))
    ((mv successp lexed warnings)
     (time$ (vl-lex preprocessed
                    :config st.config
                    :warnings (vl-loadstate->warnings st))
            :msg "~s0 (lex: ~st sec, ~sa bytes)~%"
            :args (list pad)
            :mintime st.config.mintime))
    (st (vl-loadstate-set-warnings warnings))
    ((unless successp)
     (mv (vl-loadstate-fatal :type :vl-lex-failed
                             :msg "Lexing failed for ~s0."
                             :args (list filename)
                             :st st)
         state))
    ((mv cleaned comment-map)
     (time$ (vl-kill-whitespace-and-comments lexed)
            :msg "~s0 (whitespace: ~st sec, ~sa bytes)~%"
            :args (list pad)
            :mintime st.config.mintime))
    (pstate (vl-loadstate->pstate st))
    (pstate-backup pstate)
    ((mv successp descs pstate)
     (time$ (vl-parse cleaned pstate st.config)
            :msg "; ~s0: parse: ~st sec, ~sa bytes~%"
            :args (list filename)
            :mintime st.config.mintime))
    ((unless successp)
     (b*
      ((new-warnings (vl-parsestate->warnings pstate))
       (st
        (change-vl-loadstate st
                             :pstate pstate-backup
                             :defines (make-fast-alist st.defines)))
       (st (vl-loadstate-set-warnings new-warnings))
       (st (vl-loadstate-fatal :type :vl-parse-failed
                               :msg "Parsing failed for ~s0."
                               :args (list filename)
                               :st st)))
      (mv st state)))
    (descs
       (time$ (vl-descriptionlist-inject-comments descs comment-map)
              :msg "~s0 (comment: ~st sec, ~sa bytes)~%"
              :args (list pad)
              :mintime st.config.mintime))
    ((mv descs pstate)
     (time$
          (b* ((warnings (vl-parsestate->warnings pstate))
               (warnings (vl-commentmap-translate-off-warnings
                              comment-map warnings))
               ((mv descs warnings)
                (vl-descriptionlist-inject-warnings descs warnings))
               (pstate (change-vl-parsestate pstate
                                             :warnings warnings)))
            (mv descs pstate))
          :msg "~s0 (warnings: ~st sec, ~sa bytes)~%"
          :args (list pad)
          :mintime st.config.mintime))
    ((mv descs descalist reportcard)
     (time$ (vl-load-merge-descriptions
                 descs
                 st.descs st.descalist st.reportcard)
            :msg "~s0 (merge: ~st sec, ~sa bytes)"
            :args (list pad)
            :mintime st.config.mintime))
    (st (change-vl-loadstate st
                             :pstate pstate
                             :defines defines
                             :filemap filemap
                             :iskips iskips
                             :descs descs
                             :descalist descalist
                             :reportcard reportcard)))
   (mv st state))))

Theorem: vl-loadstate-p-of-vl-load-file.st

(defthm vl-loadstate-p-of-vl-load-file.st
  (b* (((mv ?st acl2::?state)
        (vl-load-file filename st state)))
    (vl-loadstate-p st))
  :rule-classes :rewrite)

Theorem: state-p1-of-vl-load-file.state

(defthm state-p1-of-vl-load-file.state
  (implies (force (state-p1 state))
           (b* (((mv ?st acl2::?state)
                 (vl-load-file filename st state)))
             (state-p1 state)))
  :rule-classes :rewrite)

Theorem: unique-names-after-vl-load-file

(defthm unique-names-after-vl-load-file
 (b* (((mv new-st &)
       (vl-load-file filename st state)))
  (implies
   (uniquep (vl-descriptionlist->names (vl-loadstate->descs st)))
   (no-duplicatesp
        (vl-descriptionlist->names (vl-loadstate->descs new-st))))))