		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 config loc stk acc) → (mv successp morep actual remainder)
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).; config — Guard (vl-loadconfig-p config).; 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), given (force (vl-echarlist-p echars)).

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/vl2014/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 config loc stk acc)
 (declare (xargs :guard (and (stringp name)
                             (vl-echarlist-p echars)
                             (vl-loadconfig-p config)
                             (vl-location-p loc)
                             (character-listp stk)
                             (vl-echarlist-p acc))))
 (let ((__function__ 'vl-parse-define-actual))
  (declare (ignorable __function__))
  (b*
   (((when (atom echars))
     (mv
      (cw
       "Preprocessor error (~s0): unexpected end of input while processing ~
                 arguments to `~s1."
       (vl-location-string loc)
       name)
      nil "" echars))
    (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 config)))
       ((unless str)
        (mv
         (cw
          "Preprocessor error (~s0): bad string literal while processing ~
                       arguments to `~s1."
          (vl-location-string loc1)
          name)
         nil "" echars))
       (acc (revappend prefix acc)))
      (vl-parse-define-actual name remainder config loc stk acc)))
    ((when (eql char1 #\\))
     (b*
      (((mv name prefix remainder)
        (vl-read-escaped-identifier echars))
       ((unless name)
        (mv
         (cw
          "Preprocessor error (~s0): stray backslash while processing ~
                       arguments to `~s1."
          (vl-location-string loc1)
          name)
         nil "" echars))
       (acc (revappend prefix acc)))
      (vl-parse-define-actual name remainder config loc stk acc)))
    ((when (eql char1 #\/))
     (b*
      (((when (vl-matches-string-p "//" echars))
        (b*
         (((mv successp ?prefix remainder)
           (vl-read-until-literal *nls* (cddr echars)))
          ((unless successp)
           (mv
            (cw
             "Preprocessor error (~s0): unexpected EOF while reading ~
                             macro arguments to ~s1.~%"
             (vl-location-string loc1)
             name)
            nil "" echars)))
         (vl-parse-define-actual
              name remainder config loc stk acc)))
       ((when (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)))
         (vl-parse-define-actual
              name remainder config loc stk acc))))
      (vl-parse-define-actual name (cdr echars)
                              config
                              loc stk (cons (car echars) acc))))
    ((when (member char1 '(#\( #\[ #\{)))
     (b* ((stk (cons char1 stk))
          (acc (cons (car echars) acc)))
       (vl-parse-define-actual name (cdr echars)
                               config loc stk acc)))
    ((when (member char1 '(#\) #\] #\})))
     (b*
      (((when (and (eql char1 #\)) (atom stk)))
        (mv t
            nil (reverse (vl-echarlist->string acc))
            (cdr echars)))
       (matching-char (case char1 (#\) #\()
                            (#\] #\[)
                            (#\} #\{)))
       ((unless (and (consp stk)
                     (eql (car stk) matching-char)))
        (mv
         (cw
          "Preprocessor error (~s0): unbalanced ~s1 vs. ~s2 in arguments to `~s3."
          (vl-location-string loc1)
          (implode (list matching-char))
          (implode (list char1))
          name)
         nil "" echars))
       (stk (cdr stk))
       (acc (cons (car echars) acc)))
      (vl-parse-define-actual name (cdr echars)
                              config loc stk acc)))
    ((when (and (atom stk) (eql char1 #\,)))
     (mv t t (reverse (vl-echarlist->string acc))
         (cdr echars))))
   (vl-parse-define-actual name (cdr echars)
                           config
                           loc stk (cons (car echars) acc)))))

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

(defthm booleanp-of-vl-parse-define-actual.successp
  (b* (((mv ?successp ?morep ?actual ?remainder)
        (vl-parse-define-actual name echars config loc stk acc)))
    (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)
        (vl-parse-define-actual name echars config loc stk acc)))
    (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)
        (vl-parse-define-actual name echars config loc stk acc)))
    (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
 (implies
     (force (vl-echarlist-p echars))
     (b* (((mv ?successp ?morep ?actual ?remainder)
           (vl-parse-define-actual name echars config loc stk acc)))
       (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)
        (vl-parse-define-actual name echars config loc stk acc)))
    (implies successp
             (< (acl2-count remainder)
                (acl2-count echars))))
  :rule-classes ((:rewrite) (:linear)))