		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 defines istack activep) → (mv successp new-istack new-activep remainder)
Arguments: loc — Guard (vl-location-p loc).; directive — Guard (member-equal directive '("ifdef" "ifndef" "elsif")).; echars — Guard (vl-echarlist-p echars).; defines — Guard (vl-defines-p defines).; istack — Guard (vl-istack-p istack).; activep — Guard (booleanp activep).
Returns: new-istack — Type (vl-istack-p new-istack), given (and (force (vl-istack-p istack)) (force (booleanp activep))).; new-activep — Type (booleanp new-activep), given (and (force (booleanp activep)) (force (vl-istack-p istack))).; remainder — Type (vl-echarlist-p remainder), given (force (vl-echarlist-p echars)).

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 defines istack activep)
 (declare
  (xargs
    :guard (and (vl-location-p loc)
                (member-equal directive '("ifdef" "ifndef" "elsif"))
                (vl-echarlist-p echars)
                (vl-defines-p defines)
                (vl-istack-p istack)
                (booleanp activep))))
 (let ((__function__ 'vl-process-ifdef))
  (declare (ignorable __function__))
  (b*
   (((mv & remainder)
     (vl-read-while-whitespace echars))
    ((mv name & remainder)
     (vl-read-identifier remainder))
    ((unless name)
     (mv
      (cw
       "Preprocessor error (~s0): found an `~s1 without an identifier.~%"
       (vl-location-string loc)
       directive)
      istack activep echars))
    ((when (vl-is-compiler-directive-p name))
     (mv
      (cw
       "Preprocessor error (~s0): cowardly refusing to permit `s1 ~s2.~%"
       (vl-location-string loc)
       directive name)
      istack activep echars))
    ((when (equal directive "ifdef"))
     (let* ((this-satisfiedp (consp (vl-find-define name defines)))
            (new-iframe (vl-iframe activep this-satisfiedp nil))
            (new-istack (cons new-iframe istack))
            (new-activep (and activep this-satisfiedp)))
       (mv t new-istack new-activep remainder)))
    ((when (equal directive "ifndef"))
     (let* ((this-satisfiedp (not (vl-find-define name defines)))
            (new-iframe (vl-iframe activep this-satisfiedp nil))
            (new-istack (cons new-iframe istack))
            (new-activep (and activep this-satisfiedp)))
       (mv t new-istack new-activep remainder)))
    ((when (atom istack))
     (mv
      (cw
       "Preprocessor error (~s0): found an `elsif, but no ifdef or ~
                 ifndef is open.~%"
       (vl-location-string loc))
      istack activep echars))
    ((when (vl-iframe->already-saw-elsep (car istack)))
     (mv
      (cw
       "Preprocessor error (~s0): found an `elsif, but we have ~
                 already seen `else.~%"
       (vl-location-string loc))
      istack activep echars))
    (this-satisfiedp (consp (vl-find-define name defines)))
    (iframe (car istack))
    (prev-satisfiedp (vl-iframe->some-thing-satisfiedp iframe))
    (initially-activep (vl-iframe->initially-activep iframe))
    (new-activep (and this-satisfiedp (not prev-satisfiedp)
                      initially-activep))
    (new-iframe (vl-iframe initially-activep
                           (or this-satisfiedp prev-satisfiedp)
                           nil))
    (new-istack (cons new-iframe (cdr istack))))
   (mv t new-istack new-activep remainder))))

Theorem: vl-istack-p-of-vl-process-ifdef.new-istack

(defthm vl-istack-p-of-vl-process-ifdef.new-istack
  (implies (and (force (vl-istack-p istack))
                (force (booleanp activep)))
           (b* (((mv ?successp
                     ?new-istack ?new-activep ?remainder)
                 (vl-process-ifdef loc directive
                                   echars defines istack activep)))
             (vl-istack-p new-istack)))
  :rule-classes :rewrite)

Theorem: booleanp-of-vl-process-ifdef.new-activep

(defthm booleanp-of-vl-process-ifdef.new-activep
  (implies (and (force (booleanp activep))
                (force (vl-istack-p istack)))
           (b* (((mv ?successp
                     ?new-istack ?new-activep ?remainder)
                 (vl-process-ifdef loc directive
                                   echars defines istack activep)))
             (booleanp new-activep)))
  :rule-classes :rewrite)

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

(defthm vl-echarlist-p-of-vl-process-ifdef.remainder
  (implies (force (vl-echarlist-p echars))
           (b* (((mv ?successp
                     ?new-istack ?new-activep ?remainder)
                 (vl-process-ifdef loc directive
                                   echars defines istack activep)))
             (vl-echarlist-p remainder)))
  :rule-classes :rewrite)

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

(defthm true-listp-of-vl-process-ifdef
 (equal
     (true-listp
          (mv-nth 3
                  (vl-process-ifdef loc directive
                                    echars defines istack activep)))
     (true-listp echars))
 :rule-classes
 ((:rewrite)
  (:type-prescription
   :corollary
   (implies
    (true-listp echars)
    (true-listp
      (mv-nth 3
              (vl-process-ifdef loc directive
                                echars defines istack activep)))))))

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

(defthm acl2-count-of-vl-process-ifdef-weak
 (<= (acl2-count
          (mv-nth 3
                  (vl-process-ifdef loc directive
                                    echars defines istack activep)))
     (acl2-count 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 defines istack activep))
  (< (acl2-count
          (mv-nth 3
                  (vl-process-ifdef loc directive
                                    echars defines istack activep)))
     (acl2-count echars)))
 :rule-classes ((:rewrite) (:linear)))