• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
        • Preprocessor
          • Vl-iframe-p
          • Preprocessor-ifdef-minutia
          • Vl-preprocess-loop
          • Vl-read-until-end-of-define
          • Vl-expand-define
          • Vl-read-include
          • Vl-process-ifdef
          • Vl-substitute-into-macro-text
          • Vl-preprocess
          • Vl-define
          • Vl-process-define
          • Vl-process-undef
          • Preprocessor-include-minutia
          • Vl-split-define-text
          • Vl-read-timescale
          • Vl-line-up-define-formals-and-actuals
          • Vl-process-else
          • Vl-process-endif
          • Vl-istack-p
          • Vl-is-compiler-directive-p
          • Vl-check-remaining-formals-all-have-defaults
          • Vl-safe-previous-n
          • Vl-safe-next-n
          • Vl-defines
          • *vl-preprocess-clock*
        • Vl-loadconfig
        • Lexer
        • Vl-loadstate
        • Parser
        • Vl-load-merge-descriptions
        • Scope-of-defines
        • Vl-load-file
        • Vl-flush-out-descriptions
        • Vl-description
        • Vl-loadresult
        • Vl-read-file
        • Vl-find-basename/extension
        • Vl-read-files
        • Vl-find-file
        • Extended-characters
        • Vl-load
        • Vl-load-main
        • Vl-load-description
        • Vl-descriptions-left-to-load
        • Inject-warnings
        • Vl-load-descriptions
        • Vl-load-files
        • Vl-load-summary
        • Vl-collect-modules-from-descriptions
        • Vl-descriptionlist
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Preprocessor

Vl-read-until-end-of-define

Read from `define until the end of the line.

Signature

(vl-read-until-end-of-define echars config) 
  → 
(mv successp prefix remainder)

Arguments

echars — Guard (vl-echarlist-p echars).

config — Guard (vl-loadconfig-p config).

Returns

successp — Type (booleanp successp).

prefix — Type (vl-echarlist-p prefix), given (force (vl-echarlist-p echars)).

remainder — Type (vl-echarlist-p remainder), given (force (vl-echarlist-p echars)).

This is really tricky! See preprocessor-ifdef-minutia.

The initial echars are everything past the macro name, e.g., for:

`define foo blah...

the initial echars will be [space]blah..., and for

`define max(a,b) blah...

the initial echars will be (a,b) blah.... NCVerilog allows newlines within the macro arguments, e.g., it allows you to write things like

`define sum(a,
               b) a+b

But VCS rejects this. I think it's reasonable to reject this, too, so we basically just read the whole line, then split it up into any arguments versus non-arguments pieces.

Definitions and Theorems

Function: vl-read-until-end-of-define

(defun
 vl-read-until-end-of-define
 (echars config)
 (declare (xargs :guard (and (vl-echarlist-p echars)
                             (vl-loadconfig-p config))))
 (let
  ((__function__ 'vl-read-until-end-of-define))
  (declare (ignorable __function__))
  (b*
   (((when (atom echars)) (mv t nil echars))
    (char1 (vl-echar->char (first echars)))
    ((when (eql char1 #\Newline))
     (mv t nil echars))
    ((when (eql char1 #\`))
     (b*
      (((mv name prefix remainder)
        (vl-read-identifier (cdr echars)))
       ((unless name)
        (mv
         (cw
          "Preprocessor error (~s0): no name following ~
                       back-quote/grave character (`).~%"
          (vl-location-string (vl-echar->loc (car echars))))
         nil echars))
       ((when (vl-is-compiler-directive-p name))
        (mv
         (cw
          "Preprocessor error (~s0): we cowardly do not allow ~
                       `~s1 in defines.~%"
          (vl-location-string (vl-echar->loc (car echars)))
          name)
         nil echars))
       ((mv successp text remainder)
        (vl-read-until-end-of-define remainder config))
       ((unless successp) (mv nil nil echars)))
      (mv t
          (cons (car echars) (append prefix text))
          remainder)))
    ((when (eql char1 #\"))
     (b* (((mv string prefix remainder)
           (vl-read-string echars (vl-lexstate-init config)))
          ((unless string) (mv nil nil echars))
          ((mv successp text remainder)
           (vl-read-until-end-of-define remainder config))
          ((unless successp) (mv nil nil echars)))
         (mv t (append prefix text) remainder)))
    ((when (eql char1 #\\))
     (b*
      (((when (vl-matches-string-p "//" (cdr echars)))
        (mv
         (cw
          "Preprocessor error (~s0): we cowardly do not allow ~
                       '//' in defines.~%"
          (vl-location-string (vl-echar->loc (car echars))))
         nil echars))
       ((when (vl-matches-string-p "/*" (cdr echars)))
        (mv
         (cw
          "Preprocessor error (~s0): we cowardly do not allow ~
                       '/*' in defines.~%"
          (vl-location-string (vl-echar->loc (car echars))))
         nil echars))
       ((when (vl-matches-string-p *nls* (cdr echars)))
        (b* (((mv successp text remainder)
              (vl-read-until-end-of-define (cddr echars)
                                           config))
             ((unless successp) (mv nil nil echars)))
            (mv t
                (cons (change-vl-echar (second echars)
                                       :char #\Space)
                      text)
                remainder)))
       ((mv name prefix remainder)
        (vl-read-escaped-identifier echars))
       ((unless name)
        (mv (cw "Preprocessor error (~s0): stray backslash?~%"
                (vl-location-string (vl-echar->loc (car echars))))
            nil echars))
       ((mv successp text remainder)
        (vl-read-until-end-of-define remainder config))
       ((unless successp) (mv nil nil echars)))
      (mv t (append prefix text) remainder)))
    ((when (eql char1 #\/))
     (cond
      ((vl-matches-string-p "//" echars)
       (b*
        (((mv successp prefix remainder)
          (vl-read-until-literal *nls* echars))
         ((unless successp) (mv t nil remainder))
         ((when (and (consp prefix)
                     (eql (vl-echar->char (car (last prefix)))
                          #\\)))
          (mv
           (cw
            "Preprocessor error (~s0): we cowardly do not allow ~
                         single-line comments inside defines to end with .~%"
            (vl-location-string (vl-echar->loc (car echars))))
           nil echars)))
        (mv t nil remainder)))
      ((vl-matches-string-p "/*" echars)
       (b*
        (((mv successp prefix remainder)
          (vl-read-through-literal "*/" (cddr echars)))
         ((unless successp)
          (mv
           (cw
            "Preprocessor error (~s0): block comment is never ~
                         closed.~%"
            (vl-location-string (vl-echar->loc (car echars))))
           nil echars))
         ((when (member #\Newline (vl-echarlist->chars prefix)))
          (mv
           (cw
            "Preprocessor error (~s0): block comment inside a ~
                         define is not closed before end of line.~%"
            (vl-location-string (vl-echar->loc (car echars))))
           nil echars))
         ((mv successp text remainder)
          (vl-read-until-end-of-define remainder config))
         ((unless successp) (mv nil nil echars)))
        (mv t
            (append (list* (first echars)
                           (second echars)
                           prefix)
                    text)
            remainder)))
      (t (b* (((mv successp text remainder)
               (vl-read-until-end-of-define (cdr echars)
                                            config))
              ((unless successp) (mv nil nil echars)))
             (mv t (cons (car echars) text)
                 remainder)))))
    ((mv successp text remainder)
     (vl-read-until-end-of-define (cdr echars)
                                  config))
    ((unless successp) (mv nil nil echars)))
   (mv t (cons (car echars) text)
       remainder))))

Theorem: booleanp-of-vl-read-until-end-of-define.successp

(defthm booleanp-of-vl-read-until-end-of-define.successp
        (b* (((mv ?successp ?prefix ?remainder)
              (vl-read-until-end-of-define echars config)))
            (booleanp successp))
        :rule-classes :type-prescription)

Theorem: vl-echarlist-p-of-vl-read-until-end-of-define.prefix

(defthm vl-echarlist-p-of-vl-read-until-end-of-define.prefix
        (implies (force (vl-echarlist-p echars))
                 (b* (((mv ?successp ?prefix ?remainder)
                       (vl-read-until-end-of-define echars config)))
                     (vl-echarlist-p prefix)))
        :rule-classes :rewrite)

Theorem: vl-echarlist-p-of-vl-read-until-end-of-define.remainder

(defthm vl-echarlist-p-of-vl-read-until-end-of-define.remainder
        (implies (force (vl-echarlist-p echars))
                 (b* (((mv ?successp ?prefix ?remainder)
                       (vl-read-until-end-of-define echars config)))
                     (vl-echarlist-p remainder)))
        :rule-classes :rewrite)

Theorem: true-listp-of-vl-read-until-end-of-define-prefix

(defthm
   true-listp-of-vl-read-until-end-of-define-prefix
   (true-listp (mv-nth 1
                       (vl-read-until-end-of-define echars config)))
   :rule-classes :type-prescription)

Theorem: true-listp-of-vl-read-until-end-of-define-remainder

(defthm
 true-listp-of-vl-read-until-end-of-define-remainder
 (equal
   (true-listp (mv-nth 2
                       (vl-read-until-end-of-define echars config)))
   (true-listp echars))
 :rule-classes ((:rewrite)))

Theorem: acl2-count-of-vl-read-until-end-of-define-weak

(defthm
 acl2-count-of-vl-read-until-end-of-define-weak
 (<=
   (acl2-count (mv-nth 2
                       (vl-read-until-end-of-define echars config)))
   (acl2-count echars))
 :rule-classes ((:rewrite) (:linear)))

Theorem: acl2-count-of-vl-read-until-end-of-define-strong

(defthm
 acl2-count-of-vl-read-until-end-of-define-strong
 (implies
  (mv-nth 1
          (vl-read-until-end-of-define echars config))
  (<
   (acl2-count (mv-nth 2
                       (vl-read-until-end-of-define echars config)))
   (acl2-count echars)))
 :rule-classes ((:rewrite) (:linear)))