		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-preprocess-loop

Main loop for the preprocessor.

Signature
(vl-preprocess-loop echars n ppst state) → (mv successp remainder ppst state)
Arguments: echars — Guard (vl-echarlist-p echars).; n — Guard (natp n).
Returns: successp — Type (booleanp successp).; remainder — Type (vl-echarlist-p remainder).

We accumulate the transformed characters that are to be given to the lexer into acc, in reverse order.

Definitions and Theorems

Function: vl-preprocess-loop

(defun vl-preprocess-loop (echars n ppst state)
 (declare (xargs :stobjs (ppst state)))
 (declare (xargs :guard (and (vl-echarlist-p echars) (natp n))))
 (let ((__function__ 'vl-preprocess-loop))
  (declare (ignorable __function__))
  (b*
   ((echars (vl-echarlist-fix echars))
    ((when (atom echars))
     (mv t echars ppst state))
    (echar1 (car echars))
    (char1 (vl-echar->char echar1))
    ((when (zp n))
     (let
      ((ppst
        (vl-ppst-fatal
         :msg
         "~a0: ran out of steps. Macro expansion or file ~
                           inclusion loop?"
         :args (list (vl-echar->loc echar1)))))
      (mv nil echars ppst state)))
    ((when (eql char1 #\"))
     (b* (((mv string prefix remainder)
           (vl-read-string echars
                           (vl-lexstate-init (vl-ppst->config))))
          ((unless string)
           (mv nil echars ppst state))
          (ppst (vl-ppst-maybe-write prefix)))
       (vl-preprocess-loop remainder n ppst state)))
    ((when (eql char1 #\\))
     (b*
      (((mv name prefix remainder)
        (vl-read-escaped-identifier echars))
       ((unless name)
        (let
         ((ppst
               (vl-ppst-fatal :msg "~a0: stray backslash?"
                              :args (list (vl-echar->loc echar1)))))
         (mv nil echars ppst state)))
       (ppst (vl-ppst-maybe-write prefix)))
      (vl-preprocess-loop remainder n ppst state)))
    ((when (acl2::and** (eql char1 #\/)
                        (consp (cdr echars))
                        (eql (vl-echar->char (second echars))
                             #\/)))
     (if (vl-matches-string-p "@VL" (cddr echars))
         (b* (((mv atts-text remainder)
               (vl-atvl-atts-text echars))
              (atts (append (vl-echarlist-from-str "(*")
                            atts-text
                            (vl-echarlist-from-str "*)"))))
           (vl-preprocess-loop (append atts remainder)
                               (- n 1)
                               ppst state))
      (b* (((mv & prefix remainder)
            (vl-read-until-literal *nls* (cddr echars)))
           ((when (vl-matches-string-p "+VL" prefix))
            (vl-preprocess-loop (append (rest-n 3 prefix) remainder)
                                (- n 1)
                                ppst state))
           (prefix (list* (first echars)
                          (second echars)
                          prefix))
           (ppst (vl-ppst-maybe-write prefix)))
        (vl-preprocess-loop remainder n ppst state))))
    ((when (acl2::and** (eql char1 #\/)
                        (consp (cdr echars))
                        (eql (vl-echar->char (second echars))
                             #\*)))
     (b*
      (((mv successp prefix remainder)
        (vl-read-through-literal "*/" (cddr echars)))
       ((unless successp)
        (let
         ((ppst
           (vl-ppst-fatal :msg "~a0: block comment is never closed."
                          :args (list (vl-echar->loc echar1)))))
         (mv nil echars ppst state)))
       ((when (vl-matches-string-p "+VL" prefix))
        (b* ((body (butlast (rest-n 3 prefix) 2)))
          (vl-preprocess-loop (append body remainder)
                              (- n 1)
                              ppst state)))
       ((when (vl-matches-string-p "@VL" prefix))
        (b* ((body (append (vl-echarlist-from-str "(*")
                           (butlast (rest-n 3 prefix) 2)
                           (vl-echarlist-from-str "*)"))))
          (vl-preprocess-loop (append body remainder)
                              (- n 1)
                              ppst state)))
       (prefix (list* (first echars)
                      (second echars)
                      prefix))
       (ppst (vl-ppst-maybe-write prefix)))
      (vl-preprocess-loop remainder n ppst state)))
    ((unless (eql char1 #\`))
     (b* ((ppst (vl-ppst-maybe-write1 (car echars))))
       (vl-preprocess-loop (cdr echars)
                           n ppst state)))
    ((mv & remainder)
     (vl-read-while-whitespace (cdr echars)))
    ((mv directive prefix remainder)
     (vl-read-identifier remainder))
    ((unless directive)
     (let
       ((ppst (vl-ppst-fatal :msg "~a0: stray ` character."
                             :args (list (vl-echar->loc echar1)))))
       (mv nil echars ppst state)))
    ((unless (vl-is-compiler-directive-p directive))
     (b*
      ((activep (vl-ppst->activep))
       (ppst
            (vl-ppst-record-def-use
                 directive
                 (make-vl-def-context :activep activep
                                      :loc (vl-echar->loc echar1))))
       ((unless (vl-ppst->activep))
        (vl-preprocess-loop remainder n ppst state))
       ((mv successp expansion ppst)
        (vl-expand-define directive
                          remainder (vl-echar->loc echar1)
                          ppst))
       ((unless successp)
        (mv nil expansion ppst state)))
      (vl-preprocess-loop expansion (- n 1)
                          ppst state)))
    ((when (eql (vl-echar->char (car prefix)) #\\))
     (let
      ((ppst
         (vl-ppst-fatal :msg "~a0: we do not allow the use of \\~s1."
                        :args (list (vl-echar->loc echar1)
                                    directive))))
      (mv nil echars ppst state)))
    ((when (acl2::or** (equal directive "define")
                       (equal directive "centaur_define")))
     (b* (((mv successp remainder ppst)
           (vl-process-define (vl-echar->loc echar1)
                              remainder ppst))
          ((unless successp)
           (mv nil echars ppst state)))
       (vl-preprocess-loop remainder n ppst state)))
    ((when (equal directive "undef"))
     (b* (((mv successp remainder ppst)
           (vl-process-undef (vl-echar->loc echar1)
                             remainder ppst))
          ((unless successp)
           (mv nil echars ppst state)))
       (vl-preprocess-loop remainder n ppst state)))
    ((when (acl2::or** (equal directive "ifdef")
                       (equal directive "ifndef")
                       (equal directive "elsif")))
     (b* (((mv successp remainder ppst)
           (vl-process-ifdef (vl-echar->loc echar1)
                             directive remainder ppst))
          ((unless successp)
           (mv nil echars ppst state)))
       (vl-preprocess-loop remainder n ppst state)))
    ((when (equal directive "else"))
     (b* (((mv successp ppst)
           (vl-process-else (vl-echar->loc echar1)
                            ppst))
          ((unless successp)
           (mv nil echars ppst state)))
       (vl-preprocess-loop remainder n ppst state)))
    ((when (equal directive "endif"))
     (b* (((mv successp ppst)
           (vl-process-endif (vl-echar->loc echar1)
                             remainder ppst))
          ((unless successp)
           (mv nil echars ppst state)))
       (vl-preprocess-loop remainder n ppst state)))
    ((when (equal directive "include"))
     (b*
      (((unless (vl-ppst->activep))
        (vl-preprocess-loop remainder n ppst state))
       ((mv & include-line rest-of-file)
        (vl-read-until-literal *nls* remainder))
       (saved (vl-save-ppst))
       (ppst (vl-ppst-update-acc nil))
       ((mv okp ?include-line-remainder ppst state)
        (vl-preprocess-loop include-line (- n 1)
                            ppst state))
       ((vl-saved-ppst post) (vl-save-ppst))
       (ppst (vl-restore-ppst saved))
       (ppst (vl-ppst-update-defines post.defines))
       (ppst (vl-ppst-update-filemap post.filemap))
       (ppst (vl-ppst-update-iskips post.iskips))
       ((unless okp)
        (let
         ((ppst
           (vl-ppst-fatal
             :msg
             "~a0: failed to preprocess rest of `include line: ~s1."
             :args (list (vl-echar->loc echar1)
                         include-line))))
         (mv nil echars ppst state)))
       ((vl-loadconfig config)
        (vl-ppst->config))
       ((mv filename & rest-of-line ppst)
        (vl-read-include (rev post.acc) ppst))
       ((unless filename)
        (mv nil echars ppst state))
       ((mv realfile state)
        (time$ (vl-find-file filename (vl-ppst->idcache)
                             state)
               :msg "~s0: (find ~s1: ~st sec, ~sa bytes)~%"
               :args (list (vl-ppst-pad) filename)
               :mintime config.mintime))
       ((unless realfile)
        (let
         ((ppst
           (vl-ppst-fatal
            :msg
            "~a0: unable to find ~s1.  The include ~
                                 directories are ~&2."
            :args (list (vl-echar->loc echar1)
                        filename config.include-dirs))))
         (mv nil echars ppst state)))
       (controller (vl-includeskips-controller-lookup
                        realfile (vl-ppst->iskips)))
       ((when
         (acl2::and**
            controller
            (consp (vl-find-define controller (vl-ppst->defines)))))
        (b* ((iskips (vl-includeskips-record-hit
                          realfile (vl-echar->loc echar1)
                          (vl-ppst->iskips)))
             (ppst (vl-ppst-update-iskips iskips)))
          (cw-unformatted (cat (vl-ppst-pad)
                               " (skip " realfile ")" *nls*))
          (vl-preprocess-loop rest-of-file (- n 1)
                              ppst state)))
       (ppst
        (vl-maybe-ppst-warn
         :when controller
         :type :vl-warn-include-guard
         :msg
         "~a0: multiple include optimization failure: the ~
                              controlling define ~s1 is not currently ~
                              defined, so we will have to re-include ~s2."
         :args (list (vl-echar->loc echar1)
                     controller realfile)))
       (current-includes (vl-ppst->includes))
       (ppst
         (vl-ppst-update-includes (cons realfile current-includes)))
       (pad (vl-ppst-pad))
       (- (cw-unformatted (cat pad realfile *nls*)))
       ((mv okp contents len state)
        (time$ (vl-read-file (string-fix realfile))
               :msg "~s0 (read: ~st sec, ~sa bytes)~%"
               :args (list pad)
               :mintime config.mintime))
       ((unless okp)
        (let
           ((ppst (vl-ppst-fatal :msg "~a0: unable to read ~s1."
                                 :args (list (vl-echar->loc echar1)
                                             realfile))))
          (mv nil echars ppst state)))
       (ppst (vl-ppst-update-bytes (+ (vl-ppst->bytes) len)))
       (ppst (vl-maybe-update-filemap realfile contents ppst))
       (ppst (b* ((iskips (vl-includeskips-record-miss
                               realfile (vl-echar->loc echar1)
                               len (vl-ppst->iskips))))
               (vl-ppst-update-iskips iskips)))
       ((mv contents ppst)
        (vl-multiple-include-begin realfile contents ppst))
       ((mv okp remainder ppst state)
        (vl-preprocess-loop contents (- n 1)
                            ppst state))
       ((unless okp)
        (mv okp remainder ppst state))
       (ppst (vl-ppst-update-includes current-includes))
       (ppst (vl-ppst-update-acc
                  (revappend rest-of-line (vl-ppst->acc)))))
      (vl-preprocess-loop rest-of-file (- n 1)
                          ppst state)))
    ((when (equal directive "timescale"))
     (b* ((ppst (vl-ppst-maybe-write (cons echar1 prefix))))
       (vl-preprocess-loop remainder n ppst state)))
    ((when (equal directive "__FILE__"))
     (b*
      (((unless (vl-ppst->activep))
        (vl-preprocess-loop remainder n ppst state))
       ((vl-location loc)
        (vl-echar->loc echar1))
       (quoted-escaped-filename-str
            (vl-filename-to-string-literal loc.filename))
       (quoted-escaped-filename-echars
            (vl-change-echarlist-locations
                 (vl-echarlist-from-str quoted-escaped-filename-str)
                 loc))
       (ppst (vl-ppst-write quoted-escaped-filename-echars)))
      (vl-preprocess-loop remainder n ppst state)))
    ((when (equal directive "__LINE__"))
     (b* (((unless (vl-ppst->activep))
           (vl-preprocess-loop remainder n ppst state))
          ((vl-location loc)
           (vl-echar->loc echar1))
          (line-str (natstr loc.line))
          (line-echars (vl-change-echarlist-locations
                            (vl-echarlist-from-str line-str)
                            loc))
          (ppst (vl-ppst-write line-echars)))
       (vl-preprocess-loop remainder n ppst state)))
    ((when (acl2::or** (equal directive "celldefine")
                       (equal directive "endcelldefine")
                       (equal directive "resetall")
                       (equal directive "protect")
                       (equal directive "endprotect")))
     (vl-preprocess-loop remainder n ppst state))
    ((when (and (equal directive "default_nettype")
                (not (vl-ppst->activep))))
     (b* (((mv & ?prefix remainder)
           (vl-read-until-literal *nls* remainder)))
       (vl-preprocess-loop remainder n ppst state)))
    (ppst (vl-ppst-fatal :msg "~a0: we do not support `~s1."
                         :args (list (vl-echar->loc echar1)
                                     directive))))
   (mv nil echars ppst state))))

Theorem: booleanp-of-vl-preprocess-loop.successp

(defthm booleanp-of-vl-preprocess-loop.successp
  (b* (((mv ?successp ?remainder ?ppst acl2::?state)
        (vl-preprocess-loop echars n ppst state)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: vl-echarlist-p-of-vl-preprocess-loop.remainder

(defthm vl-echarlist-p-of-vl-preprocess-loop.remainder
  (b* (((mv ?successp ?remainder ?ppst acl2::?state)
        (vl-preprocess-loop echars n ppst state)))
    (vl-echarlist-p remainder))
  :rule-classes :rewrite)

Theorem: state-p1-of-vl-preprocess-loop

(defthm state-p1-of-vl-preprocess-loop
  (implies (force (state-p1 state))
           (b* (((mv ?successp ?echars ?ppst state)
                 (vl-preprocess-loop echars n ppst state)))
             (state-p1 state))))