		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)
    (warnings (vl-parsestate->warnings st.pstate))
    ((mv okp contents state)
     (time$ (vl-read-file (string-fix filename))
            :msg "; ~s0: read: ~st sec, ~sa bytes~%"
            :args (list filename)
            :mintime st.config.mintime))
    ((unless okp)
     (b* ((warnings (warn :type :vl-read-failed
                          :msg "Error reading file ~s0."
                          :args (list filename))))
       (mv (vl-loadstate-set-warnings warnings)
           state)))
    (filemap
         (time$ (and st.config.filemapp
                     (cons (cons filename
                                 (vl-echarlist->string contents))
                           st.filemap))
                :msg "; ~s0: filemap: ~st sec, ~sa bytes~%"
                :args (list filename)
                :mintime st.config.mintime))
    ((mv successp
         defines filemap preprocessed state)
     (time$ (vl-preprocess contents
                           :defines st.defines
                           :filemap filemap
                           :config st.config)
            :msg "; ~s0: preprocess: ~st sec, ~sa bytes~%"
            :args (list filename)
            :mintime st.config.mintime))
    ((unless successp)
     (b* ((warnings (warn :type :vl-preprocess-failed
                          :msg "Preprocessing failed for ~s0."
                          :args (list filename))))
       (mv (vl-loadstate-set-warnings warnings)
           state)))
    ((mv successp lexed warnings)
     (time$ (vl-lex preprocessed
                    :config st.config
                    :warnings warnings)
            :msg "; ~s0: lex: ~st sec, ~sa bytes~%"
            :args (list filename)
            :mintime st.config.mintime))
    ((unless successp)
     (b* ((warnings (warn :type :vl-lex-failed
                          :msg "Lexing failed for ~s0."
                          :args (list filename))))
       (mv (vl-loadstate-set-warnings warnings)
           state)))
    ((mv cleaned comment-map)
     (time$ (vl-kill-whitespace-and-comments lexed)
            :msg "; ~s0: whitespace: ~st sec, ~sa bytes~%"
            :args (list filename)
            :mintime st.config.mintime))
    (pstate (change-vl-parsestate st.pstate
                                  :warnings warnings))
    (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* ((- (vl-parsestate-free pstate))
          (pstate (vl-parsestate-restore pstate-backup))
          (w (make-vl-warning :type :vl-parse-failed
                              :msg "Parsing failed for ~s0."
                              :args (list filename)
                              :fn __function__))
          (pstate (vl-parsestate-add-warning w pstate))
          (st (change-vl-loadstate st
                                   :pstate pstate)))
       (mv st state)))
    (descs
       (time$ (vl-descriptionlist-inject-comments descs comment-map)
              :msg "; ~s0: comment: ~st sec, ~sa bytes~%"
              :args (list filename)
              :mintime st.config.mintime))
    ((mv descs pstate)
     (b* ((warnings (vl-parsestate->warnings pstate))
          ((mv descs warnings)
           (vl-descriptionlist-inject-warnings descs warnings))
          (pstate (change-vl-parsestate pstate
                                        :warnings warnings)))
       (mv descs pstate)))
    ((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 filename)
            :mintime st.config.mintime))
    (st (change-vl-loadstate st
                             :pstate pstate
                             :defines defines
                             :filemap filemap
                             :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))))))