		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Vl-process-ifdef

Handler for ifdef, ifndef, and elsif directives.

Signature
(vl-process-ifdef loc directive echars ppst) → (mv successp remainder ppst)
Arguments: loc — Guard (vl-location-p loc).; directive — Guard (member-equal directive '("ifdef" "ifndef" "elsif")).; echars — Guard (vl-echarlist-p echars).
Returns: remainder — Type (vl-echarlist-p remainder).

We assume that we have just read `directive from echars. We need to read the identifier that should follow this directive, look it up in the defines table, and make the appropriate changes to the istack and activep.

Definitions and Theorems

Function: vl-process-ifdef

(defun vl-process-ifdef (loc directive echars ppst)
 (declare (xargs :stobjs (ppst)))
 (declare
  (xargs
    :guard (and (vl-location-p loc)
                (member-equal directive '("ifdef" "ifndef" "elsif"))
                (vl-echarlist-p echars))))
 (let ((__function__ 'vl-process-ifdef))
  (declare (ignorable __function__))
  (b*
   ((echars (vl-echarlist-fix echars))
    ((mv & remainder)
     (vl-read-while-whitespace echars))
    ((mv name & remainder)
     (vl-read-identifier remainder))
    ((unless name)
     (let
       ((ppst (vl-ppst-fatal
                   :msg "~a0: found an `~s1 without an identifier."
                   :args (list loc directive))))
       (mv nil echars ppst)))
    ((when (vl-is-compiler-directive-p name))
     (let
       ((ppst (vl-ppst-fatal
                   :msg "~a0: cowardly refusing to permit `s1 ~s2."
                   :args (list loc directive name))))
       (mv nil echars ppst)))
    (activep (vl-ppst->activep))
    (defines (vl-ppst->defines))
    (istack (vl-ppst->istack))
    ((when (equal directive "ifdef"))
     (let*
       ((this-satisfiedp (consp (vl-find-define name defines)))
        (new-iframe
             (make-vl-iframe :initially-activep activep
                             :some-thing-satisfiedp this-satisfiedp
                             :already-saw-elsep nil
                             :mi-controller nil
                             :mi-filename nil))
        (new-istack (cons new-iframe istack))
        (new-activep (and activep this-satisfiedp))
        (new-ctx (make-vl-ifdef-context :loc loc))
        (ppst (vl-ppst-update-istack new-istack))
        (ppst (vl-ppst-record-ifdef-use name new-ctx))
        (ppst (vl-ppst-update-activep new-activep)))
       (mv t remainder ppst)))
    ((when (equal directive "ifndef"))
     (let*
       ((this-satisfiedp (not (vl-find-define name defines)))
        (new-iframe
             (make-vl-iframe :initially-activep activep
                             :some-thing-satisfiedp this-satisfiedp
                             :already-saw-elsep nil
                             :mi-controller nil
                             :mi-filename nil))
        (new-istack (cons new-iframe istack))
        (new-activep (and activep this-satisfiedp))
        (new-ctx (make-vl-ifdef-context :loc loc))
        (ppst (vl-ppst-update-istack new-istack))
        (ppst (vl-ppst-record-ifdef-use name new-ctx))
        (ppst (vl-ppst-update-activep new-activep)))
       (mv t remainder ppst)))
    ((when (atom istack))
     (let
       ((ppst (vl-ppst-fatal
                   :msg "~a0: found `elsif, but no `ifdef is open."
                   :args (list loc))))
       (mv nil echars ppst)))
    ((vl-iframe iframe) (car istack))
    ((when iframe.already-saw-elsep)
     (let
      ((ppst
        (vl-ppst-fatal
           :msg "~a0: found `elsif, but we have already seen `else."
           :args (list loc))))
      (mv nil echars ppst)))
    (ppst
     (vl-maybe-ppst-warn
      :when iframe.mi-controller
      :type :vl-warn-include-guard
      :msg
      "~a0: suppressing multiple-include optimization due to ~
                      `elsif."
      :args (list loc)))
    (this-satisfiedp (consp (vl-find-define name defines)))
    (new-activep (and this-satisfiedp
                      (not iframe.some-thing-satisfiedp)
                      iframe.initially-activep))
    (new-iframe
       (change-vl-iframe
            iframe
            :some-thing-satisfiedp (or this-satisfiedp
                                       iframe.some-thing-satisfiedp)
            :mi-controller nil
            :mi-filename nil))
    (new-ctx (make-vl-ifdef-context :loc loc))
    (new-istack (cons new-iframe (cdr istack)))
    (ppst (vl-ppst-update-activep new-activep))
    (ppst (vl-ppst-record-ifdef-use name new-ctx))
    (ppst (vl-ppst-update-istack new-istack)))
   (mv t remainder ppst))))

Theorem: vl-echarlist-p-of-vl-process-ifdef.remainder

(defthm vl-echarlist-p-of-vl-process-ifdef.remainder
  (b* (((mv ?successp ?remainder ?ppst)
        (vl-process-ifdef loc directive echars ppst)))
    (vl-echarlist-p remainder))
  :rule-classes :rewrite)

Theorem: true-listp-of-vl-process-ifdef

(defthm true-listp-of-vl-process-ifdef
  (true-listp (mv-nth 1
                      (vl-process-ifdef loc directive echars ppst)))
  :rule-classes :type-prescription)

Theorem: acl2-count-of-vl-process-ifdef-weak

(defthm acl2-count-of-vl-process-ifdef-weak
 (<=
  (acl2-count (mv-nth 1
                      (vl-process-ifdef loc directive echars ppst)))
  (acl2-count (vl-echarlist-fix echars)))
 :rule-classes ((:rewrite) (:linear)))

Theorem: acl2-count-of-vl-process-ifdef-strong

(defthm acl2-count-of-vl-process-ifdef-strong
 (implies
      (mv-nth 0
              (vl-process-ifdef loc directive echars ppst))
      (< (acl2-count
              (mv-nth 1
                      (vl-process-ifdef loc directive echars ppst)))
         (acl2-count (vl-echarlist-fix echars))))
 :rule-classes ((:rewrite) (:linear)))