		Search-engine friendly clone of the ACL2 documentation.

Vl-expand-define

Vl-parse-define-actual

Collect a single argument to a text macro, like `max(a+b, c).

Signature
(vl-parse-define-actual name echars loc stk acc ppst) → (mv successp morep actual remainder ppst)
Arguments: name — Name of macro being expanded, e.g., max, for error messages.
Guard (stringp name).; echars — Text we're parsing, initially follows an open paren or comma.
Guard (vl-echarlist-p echars).; loc — Location information in case of error messages.
Guard (vl-location-p loc).; stk — Stack of open paren/bracket/brace characters.
Guard (character-listp stk).; acc — Text we've matched so far.
Guard (vl-echarlist-p acc).
Returns: successp — Was there any error?.
Type (booleanp successp).; morep — Is this the last actual?.
Type (booleanp morep).; actual — Contents of the actual as a string.
Type (stringp actual).; remainder — Remaining characters past the comma/closing paren.
Type (vl-echarlist-p remainder).

SystemVerilog-2012 gives the following grammar (Page 641, Syntax 22-3):

text_macro_usage ::= text_macro_identifier [ '(' list_of_actual_arguments ')' ]

list_of_actual_arguments ::= actual_argument { ',' actual_argument }

actual_argument ::= expression

But this last part is clearly total bullshit. For instance on page 643 we are told:

"However, one can define an empty text macro, say `EMPTY, and use that as an actual argument. This will be substituted in place of the formal argument and will be replaced by empty text after expansion of the empty text macro."

It seems very clear that the empty string is not an expression. Moreover, all of this discussion of the preprocessor seems quite deeply rooted in a notion of textual substitution. Accordingly, the idea that actual_argument ::= expression seems to be very much confusing different levels of representation (e.g., expressions versus text) and just cannot be correct at all.

That's a bummer because we need to allow something to occur in these actuals, and that something could be some rather complicated piece of text. Interestingly, both NCVerilog and VCS permit uses of macros such as:

`define identity(a) a
module foo;
  `identity(reg foo;)
endmodule

However they complain about too many macro arguments on examples such as:

`identity(reg bar, baz;)

Meanwhile they happily accept syntax such as:

`identity(2 + {1'b0, 1'b1

})

On Page 641 of the spec, we find some hints about what might be permitted here:

"Actual arguments and defaults shall not contain comma or right parenthesis characters outside matched pairs of left and right parentheses (), square brackets [], braces {}, double quotes ", or an escaped identifier."

This paragraph seems to suggest a kind of algorithm for deciding where the actual text ends, roughly: keep track of matched pairs of these special characters, be smart enough to recognize strings and escaped identifiers, and stop when you see a comma or right parenthesis.

I implement such an algorithm here, but of course there is a great deal of room for ambiguity and confusion here, so this may well not be at all correct. The system tests (centaur/vl/systest) do try to test some tricky cases, but there may well be mismatches left.

Definitions and Theorems

Function: vl-parse-define-actual

(defun vl-parse-define-actual (name echars loc stk acc ppst)
 (declare (xargs :stobjs (ppst)))
 (declare (xargs :guard (and (stringp name)
                             (vl-echarlist-p echars)
                             (vl-location-p loc)
                             (character-listp stk)
                             (vl-echarlist-p acc))))
 (let ((__function__ 'vl-parse-define-actual))
  (declare (ignorable __function__))
  (b*
   ((echars (vl-echarlist-fix echars))
    ((when (atom echars))
     (let
      ((ppst
        (vl-ppst-fatal
         :msg
         "~a0: unexpected end of input while processing ~
                           arguments to `~s1."
         :args (list loc name))))
      (mv nil nil "" echars ppst)))
    (char1 (vl-echar->char (car echars)))
    (loc1 (vl-echar->loc (car echars)))
    ((when (eql char1 #\"))
     (b*
      (((mv str prefix remainder)
        (vl-read-string echars
                        (vl-lexstate-init (vl-ppst->config))))
       ((unless str)
        (let
         ((ppst
           (vl-ppst-fatal
            :msg
            "~a0: bad string literal while processing ~
                                 arguments to `~s1."
            :args (list loc1 name))))
         (mv nil nil "" echars ppst)))
       (acc (revappend prefix acc)))
      (vl-parse-define-actual name remainder loc stk acc ppst)))
    ((when (and (eql char1 #\`)
                (consp (cdr echars))
                (eql (vl-echar->char (second echars))
                     #\")))
     (b*
      (((mv str prefix remainder)
        (vl-read-string (cdr echars)
                        (vl-lexstate-init (vl-ppst->config))))
       ((unless str)
        (let
         ((ppst
           (vl-ppst-fatal
            :msg
            "~a0: bad string literal while processing ~
                                 arguments to `~s1."
            :args (list loc1 name))))
         (mv nil nil "" echars ppst)))
       (len (length str))
       ((unless (and (< 0 len)
                     (equal (char str (- len 1)) #\`)))
        (let
         ((ppst
           (vl-ppst-fatal
            :msg
            "~a0: found string literal with backtick-escaped ~
                                 open quote but regular closing quote, i.e., ~
                                 `\"...\", while processing arguments to ~s1."
            :args (list loc1 name))))
         (mv nil nil "" echars ppst)))
       (rprefix (rev prefix))
       (rprefix-fixed (cons (first rprefix) (cddr rprefix)))
       (acc (append rprefix-fixed acc)))
      (vl-parse-define-actual name remainder loc stk acc ppst)))
    ((when (eql char1 #\\))
     (b*
      (((mv name prefix remainder)
        (vl-read-escaped-identifier echars))
       ((unless name)
        (let
         ((ppst
           (vl-ppst-fatal
            :msg
            "~a0:  stray backslash while processing ~
                                 arguments to `~s1."
            :args (list loc1 name))))
         (mv nil nil "" echars ppst)))
       (acc (revappend prefix acc)))
      (vl-parse-define-actual name remainder loc stk acc ppst)))
    ((when (eql char1 #\/))
     (b*
      (((when (vl-matches-string-p "//" echars))
        (b*
         (((mv successp ?prefix remainder)
           (vl-read-until-literal *nls* (cddr echars)))
          ((unless successp)
           (let
            ((ppst
              (vl-ppst-fatal
               :msg
               "~a0: unexpected EOF while reading ~
                                       macro arguments to ~s1."
               :args (list loc1 name))))
            (mv nil nil "" echars ppst))))
         (vl-parse-define-actual name remainder loc stk acc ppst)))
       ((when (vl-matches-string-p "/*" 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 (car echars))))))
            (mv nil nil "" echars ppst))))
         (vl-parse-define-actual name remainder loc stk acc ppst))))
      (vl-parse-define-actual name (cdr echars)
                              loc stk (cons (car echars) acc)
                              ppst)))
    ((when (member char1 '(#\( #\[ #\{)))
     (b* ((stk (cons char1 stk))
          (acc (cons (car echars) acc)))
       (vl-parse-define-actual name (cdr echars)
                               loc stk acc ppst)))
    ((when (member char1 '(#\) #\] #\})))
     (b*
      (((when (and (eql char1 #\)) (atom stk)))
        (mv t
            nil (reverse (vl-echarlist->string acc))
            (cdr echars)
            ppst))
       (matching-char (case char1 (#\) #\()
                            (#\] #\[)
                            (#\} #\{)))
       ((unless (and (consp stk)
                     (eql (car stk) matching-char)))
        (let
         ((ppst
           (vl-ppst-fatal
            :msg "~a0: unbalanced ~s1 vs. ~s2 in arguments to `~s3."
            :args (list loc1 (implode (list matching-char))
                        (implode (list char1))
                        name))))
         (mv nil nil "" echars ppst)))
       (stk (cdr stk))
       (acc (cons (car echars) acc)))
      (vl-parse-define-actual name (cdr echars)
                              loc stk acc ppst)))
    ((when (and (atom stk) (eql char1 #\,)))
     (mv t t (reverse (vl-echarlist->string acc))
         (cdr echars)
         ppst)))
   (vl-parse-define-actual name (cdr echars)
                           loc stk (cons (car echars) acc)
                           ppst))))

Theorem: booleanp-of-vl-parse-define-actual.successp

(defthm booleanp-of-vl-parse-define-actual.successp
  (b* (((mv ?successp
            ?morep ?actual ?remainder ?ppst)
        (vl-parse-define-actual name echars loc stk acc ppst)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: booleanp-of-vl-parse-define-actual.morep

(defthm booleanp-of-vl-parse-define-actual.morep
  (b* (((mv ?successp
            ?morep ?actual ?remainder ?ppst)
        (vl-parse-define-actual name echars loc stk acc ppst)))
    (booleanp morep))
  :rule-classes :type-prescription)

Theorem: stringp-of-vl-parse-define-actual.actual

(defthm stringp-of-vl-parse-define-actual.actual
  (b* (((mv ?successp
            ?morep ?actual ?remainder ?ppst)
        (vl-parse-define-actual name echars loc stk acc ppst)))
    (stringp actual))
  :rule-classes :type-prescription)

Theorem: vl-echarlist-p-of-vl-parse-define-actual.remainder

(defthm vl-echarlist-p-of-vl-parse-define-actual.remainder
  (b* (((mv ?successp
            ?morep ?actual ?remainder ?ppst)
        (vl-parse-define-actual name echars loc stk acc ppst)))
    (vl-echarlist-p remainder))
  :rule-classes :rewrite)

Theorem: acl2-count-of-vl-parse-define-actual

(defthm acl2-count-of-vl-parse-define-actual
  (b* (((mv successp ?morep ?actual remainder ?ppst)
        (vl-parse-define-actual name echars loc stk acc ppst)))
    (implies successp
             (< (acl2-count remainder)
                (acl2-count (vl-echarlist-fix echars)))))
  :rule-classes ((:rewrite) (:linear)))