sys/src/cmd/spin/spin.y

   1 /***** spin: spin.y *****/
   2
   3 /* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories.     */
   4 /* All Rights Reserved.  This software is for educational purposes only.  */
   5 /* No guarantee whatsoever is expressed or implied by the distribution of */
   6 /* this code.  Permission is given to distribute this code provided that  */
   7 /* this introductory message is not removed and no monies are exchanged.  */
   8 /* Software written by Gerard J. Holzmann.  For tool documentation see:   */
   9 /*             http://spinroot.com/                                       */
  10 /* Send all bug-reports and/or questions to: bugs@spinroot.com            */
  11
  12 %{
  13 #include "spin.h"
  14 #include <stdarg.h>
  15
  16 #define YYDEBUG 0
  17 #define Stop    nn(ZN,'@',ZN,ZN)
  18
  19 extern  Symbol  *context, *owner;
  20 extern  int     u_sync, u_async, dumptab;
  21 extern  short   has_sorted, has_random, has_enabled, has_pcvalue, has_np;
  22 extern  short   has_code, has_state, has_io;
  23 extern  void    count_runs(Lextok *);
  24 extern  void    no_internals(Lextok *);
  25 extern  void    any_runs(Lextok *);
  26 extern  void    validref(Lextok *, Lextok *);
  27 extern  char    yytext[];
  28
  29 int     Mpars = 0;      /* max nr of message parameters  */
  30 int     runsafe = 1;    /* 1 if all run stmnts are in init */
  31 int     Expand_Ok = 0, realread = 1, IArgs = 0, NamesNotAdded = 0;
  32 char    *claimproc = (char *) 0;
  33 char    *eventmap = (char *) 0;
  34
  35 static  int     Embedded = 0, inEventMap = 0, has_ini = 0;
  36
  37 %}
  38
  39 %token  ASSERT PRINT PRINTM
  40 %token  C_CODE C_DECL C_EXPR C_STATE C_TRACK
  41 %token  RUN LEN ENABLED EVAL PC_VAL
  42 %token  TYPEDEF MTYPE INLINE LABEL OF
  43 %token  GOTO BREAK ELSE SEMI
  44 %token  IF FI DO OD SEP
  45 %token  ATOMIC NON_ATOMIC D_STEP UNLESS
  46 %token  TIMEOUT NONPROGRESS
  47 %token  ACTIVE PROCTYPE D_PROCTYPE
  48 %token  HIDDEN SHOW ISLOCAL
  49 %token  PRIORITY PROVIDED
  50 %token  FULL EMPTY NFULL NEMPTY
  51 %token  CONST TYPE XU                   /* val */
  52 %token  NAME UNAME PNAME INAME          /* sym */
  53 %token  STRING CLAIM TRACE INIT         /* sym */
  54
  55 %right  ASGN
  56 %left   SND O_SND RCV R_RCV /* SND doubles as boolean negation */
  57 %left   OR
  58 %left   AND
  59 %left   '|'
  60 %left   '^'
  61 %left   '&'
  62 %left   EQ NE
  63 %left   GT LT GE LE
  64 %left   LSHIFT RSHIFT
  65 %left   '+' '-'
  66 %left   '*' '/' '%'
  67 %left   INCR DECR
  68 %right  '~' UMIN NEG
  69 %left   DOT
  70 %%
  71
  72 /** PROMELA Grammar Rules **/
  73
  74 program : units         { yytext[0] = '\0'; }
  75         ;
  76
  77 units   : unit
  78         | units unit
  79         ;
  80
  81 unit    : proc          /* proctype { }       */
  82         | init          /* init { }           */
  83         | claim         /* never claim        */
  84         | events        /* event assertions   */
  85         | one_decl      /* variables, chans   */
  86         | utype         /* user defined types */
  87         | c_fcts        /* c functions etc.   */
  88         | ns            /* named sequence     */
  89         | SEMI          /* optional separator */
  90         | error
  91         ;
  92
  93 proc    : inst          /* optional instantiator */
  94           proctype NAME {
  95                           setptype($3, PROCTYPE, ZN);
  96                           setpname($3);
  97                           context = $3->sym;
  98                           context->ini = $2; /* linenr and file */
  99                           Expand_Ok++; /* expand struct names in decl */
 100                           has_ini = 0;
 101                         }
 102           '(' decl ')'  { Expand_Ok--;
 103                           if (has_ini)
 104                           fatal("initializer in parameter list", (char *) 0);
 105                         }
 106           Opt_priority
 107           Opt_enabler
 108           body          { ProcList *rl;
 109                           rl = ready($3->sym, $6, $11->sq, $2->val, $10);
 110                           if ($1 != ZN && $1->val > 0)
 111                           {     int j;
 112                                 for (j = 0; j < $1->val; j++)
 113                                 runnable(rl, $9?$9->val:1, 1);
 114                                 announce(":root:");
 115                                 if (dumptab) $3->sym->ini = $1;
 116                           }
 117                           context = ZS;
 118                         }
 119         ;
 120
 121 proctype: PROCTYPE      { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 0; }
 122         | D_PROCTYPE    { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 1; }
 123         ;
 124
 125 inst    : /* empty */   { $$ = ZN; }
 126         | ACTIVE        { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 1; }
 127         | ACTIVE '[' CONST ']' {
 128                           $$ = nn(ZN,CONST,ZN,ZN); $$->val = $3->val;
 129                           if ($3->val > 255)
 130                                 non_fatal("max nr of processes is 255\n", "");
 131                         }
 132         | ACTIVE '[' NAME ']' {
 133                           $$ = nn(ZN,CONST,ZN,ZN);
 134                           $$->val = 0;
 135                           if (!$3->sym->type)
 136                                 non_fatal("undeclared variable %s",
 137                                         $3->sym->name);
 138                           else if ($3->sym->ini->ntyp != CONST)
 139                                 non_fatal("need constant initializer for %s\n",
 140                                         $3->sym->name);
 141                           else
 142                                 $$->val = $3->sym->ini->val;
 143                         }
 144         ;
 145
 146 init    : INIT          { context = $1->sym; }
 147           Opt_priority
 148           body          { ProcList *rl;
 149                           rl = ready(context, ZN, $4->sq, 0, ZN);
 150                           runnable(rl, $3?$3->val:1, 1);
 151                           announce(":root:");
 152                           context = ZS;
 153                         }
 154         ;
 155
 156 claim   : CLAIM         { context = $1->sym;
 157                           if (claimproc)
 158                                 non_fatal("claim %s redefined", claimproc);
 159                           claimproc = $1->sym->name;
 160                         }
 161           body          { (void) ready($1->sym, ZN, $3->sq, 0, ZN);
 162                           context = ZS;
 163                         }
 164         ;
 165
 166 events : TRACE          { context = $1->sym;
 167                           if (eventmap)
 168                                 non_fatal("trace %s redefined", eventmap);
 169                           eventmap = $1->sym->name;
 170                           inEventMap++;
 171                         }
 172           body          { (void) ready($1->sym, ZN, $3->sq, 0, ZN);
 173                           context = ZS;
 174                           inEventMap--;
 175                         }
 176         ;
 177
 178 utype   : TYPEDEF NAME          { if (context)
 179                                    fatal("typedef %s must be global",
 180                                                 $2->sym->name);
 181                                    owner = $2->sym;
 182                                 }
 183           '{' decl_lst '}'      { setuname($5); owner = ZS; }
 184         ;
 185
 186 nm      : NAME                  { $$ = $1; }
 187         | INAME                 { $$ = $1;
 188                                   if (IArgs)
 189                                   fatal("invalid use of '%s'", $1->sym->name);
 190                                 }
 191         ;
 192
 193 ns      : INLINE nm '('         { NamesNotAdded++; }
 194           args ')'              { prep_inline($2->sym, $5);
 195                                   NamesNotAdded--;
 196                                 }
 197         ;
 198
 199 c_fcts  : ccode                 { /* leaves pseudo-inlines with sym of
 200                                    * type CODE_FRAG or CODE_DECL in global context
 201                                    */
 202                                 }
 203         | cstate
 204         ;
 205
 206 cstate  : C_STATE STRING STRING {
 207                                   c_state($2->sym, $3->sym, ZS);
 208                                   has_code = has_state = 1;
 209                                 }
 210         | C_TRACK STRING STRING {
 211                                   c_track($2->sym, $3->sym, ZS);
 212                                   has_code = has_state = 1;
 213                                 }
 214         | C_STATE STRING STRING STRING {
 215                                   c_state($2->sym, $3->sym, $4->sym);
 216                                   has_code = has_state = 1;
 217                                 }
 218         | C_TRACK STRING STRING STRING {
 219                                   c_track($2->sym, $3->sym, $4->sym);
 220                                   has_code = has_state = 1;
 221                                 }
 222         ;
 223
 224 ccode   : C_CODE                { Symbol *s;
 225                                   NamesNotAdded++;
 226                                   s = prep_inline(ZS, ZN);
 227                                   NamesNotAdded--;
 228                                   $$ = nn(ZN, C_CODE, ZN, ZN);
 229                                   $$->sym = s;
 230                                   has_code = 1;
 231                                 }
 232         | C_DECL                { Symbol *s;
 233                                   NamesNotAdded++;
 234                                   s = prep_inline(ZS, ZN);
 235                                   NamesNotAdded--;
 236                                   s->type = CODE_DECL;
 237                                   $$ = nn(ZN, C_CODE, ZN, ZN);
 238                                   $$->sym = s;
 239                                   has_code = 1;
 240                                 }
 241         ;
 242 cexpr   : C_EXPR                { Symbol *s;
 243                                   NamesNotAdded++;
 244                                   s = prep_inline(ZS, ZN);
 245                                   NamesNotAdded--;
 246                                   $$ = nn(ZN, C_EXPR, ZN, ZN);
 247                                   $$->sym = s;
 248                                   no_side_effects(s->name);
 249                                   has_code = 1;
 250                                 }
 251         ;
 252
 253 body    : '{'                   { open_seq(1); }
 254           sequence OS           { add_seq(Stop); }
 255           '}'                   { $$->sq = close_seq(0); }
 256         ;
 257
 258 sequence: step                  { if ($1) add_seq($1); }
 259         | sequence MS step      { if ($3) add_seq($3); }
 260         ;
 261
 262 step    : one_decl              { $$ = ZN; }
 263         | XU vref_lst           { setxus($2, $1->val); $$ = ZN; }
 264         | NAME ':' one_decl     { fatal("label preceding declaration,", (char *)0); }
 265         | NAME ':' XU           { fatal("label predecing xr/xs claim,", 0); }
 266         | stmnt                 { $$ = $1; }
 267         | stmnt UNLESS stmnt    { $$ = do_unless($1, $3); }
 268         ;
 269
 270 vis     : /* empty */           { $$ = ZN; }
 271         | HIDDEN                { $$ = $1; }
 272         | SHOW                  { $$ = $1; }
 273         | ISLOCAL               { $$ = $1; }
 274         ;
 275
 276 asgn:   /* empty */
 277         | ASGN
 278         ;
 279
 280 one_decl: vis TYPE var_list     { setptype($3, $2->val, $1); $$ = $3; }
 281         | vis UNAME var_list    { setutype($3, $2->sym, $1);
 282                                   $$ = expand($3, Expand_Ok);
 283                                 }
 284         | vis TYPE asgn '{' nlst '}' {
 285                                   if ($2->val != MTYPE)
 286                                         fatal("malformed declaration", 0);
 287                                   setmtype($5);
 288                                   if ($1)
 289                                         non_fatal("cannot %s mtype (ignored)",
 290                                                 $1->sym->name);
 291                                   if (context != ZS)
 292                                         fatal("mtype declaration must be global", 0);
 293                                 }
 294         ;
 295
 296 decl_lst: one_decl              { $$ = nn(ZN, ',', $1, ZN); }
 297         | one_decl SEMI
 298           decl_lst              { $$ = nn(ZN, ',', $1, $3); }
 299         ;
 300
 301 decl    : /* empty */           { $$ = ZN; }
 302         | decl_lst              { $$ = $1; }
 303         ;
 304
 305 vref_lst: varref                { $$ = nn($1, XU, $1, ZN); }
 306         | varref ',' vref_lst   { $$ = nn($1, XU, $1, $3); }
 307         ;
 308
 309 var_list: ivar                  { $$ = nn($1, TYPE, ZN, ZN); }
 310         | ivar ',' var_list     { $$ = nn($1, TYPE, ZN, $3); }
 311         ;
 312
 313 ivar    : vardcl                { $$ = $1;
 314                                   $1->sym->ini = nn(ZN,CONST,ZN,ZN);
 315                                   $1->sym->ini->val = 0;
 316                                 }
 317         | vardcl ASGN expr      { $1->sym->ini = $3; $$ = $1;
 318                                   trackvar($1,$3); has_ini = 1;
 319                                 }
 320         | vardcl ASGN ch_init   { $1->sym->ini = $3;
 321                                   $$ = $1; has_ini = 1;
 322                                 }
 323         ;
 324
 325 ch_init : '[' CONST ']' OF
 326           '{' typ_list '}'      { if ($2->val) u_async++;
 327                                   else u_sync++;
 328                                   {     int i = cnt_mpars($6);
 329                                         Mpars = max(Mpars, i);
 330                                   }
 331                                   $$ = nn(ZN, CHAN, ZN, $6);
 332                                   $$->val = $2->val;
 333                                 }
 334         ;
 335
 336 vardcl  : NAME                  { $1->sym->nel = 1; $$ = $1; }
 337         | NAME ':' CONST        { $1->sym->nbits = $3->val;
 338                                   if ($3->val >= 8*sizeof(long))
 339                                   {     non_fatal("width-field %s too large",
 340                                                 $1->sym->name);
 341                                         $3->val = 8*sizeof(long)-1;
 342                                   }
 343                                   $1->sym->nel = 1; $$ = $1;
 344                                 }
 345         | NAME '[' CONST ']'    { $1->sym->nel = $3->val; $$ = $1; }
 346         ;
 347
 348 varref  : cmpnd                 { $$ = mk_explicit($1, Expand_Ok, NAME); }
 349         ;
 350
 351 pfld    : NAME                  { $$ = nn($1, NAME, ZN, ZN); }
 352         | NAME                  { owner = ZS; }
 353           '[' expr ']'          { $$ = nn($1, NAME, $4, ZN); }
 354         ;
 355
 356 cmpnd   : pfld                  { Embedded++;
 357                                   if ($1->sym->type == STRUCT)
 358                                         owner = $1->sym->Snm;
 359                                 }
 360           sfld                  { $$ = $1; $$->rgt = $3;
 361                                   if ($3 && $1->sym->type != STRUCT)
 362                                         $1->sym->type = STRUCT;
 363                                   Embedded--;
 364                                   if (!Embedded && !NamesNotAdded
 365                                   &&  !$1->sym->type)
 366                                    non_fatal("undeclared variable: %s",
 367                                                 $1->sym->name);
 368                                   if ($3) validref($1, $3->lft);
 369                                   owner = ZS;
 370                                 }
 371         ;
 372
 373 sfld    : /* empty */           { $$ = ZN; }
 374         | '.' cmpnd %prec DOT   { $$ = nn(ZN, '.', $2, ZN); }
 375         ;
 376
 377 stmnt   : Special               { $$ = $1; }
 378         | Stmnt                 { $$ = $1;
 379                                   if (inEventMap)
 380                                    non_fatal("not an event", (char *)0);
 381                                 }
 382         ;
 383
 384 Special : varref RCV            { Expand_Ok++; }
 385           rargs                 { Expand_Ok--; has_io++;
 386                                   $$ = nn($1,  'r', $1, $4);
 387                                   trackchanuse($4, ZN, 'R');
 388                                 }
 389         | varref SND            { Expand_Ok++; }
 390           margs                 { Expand_Ok--; has_io++;
 391                                   $$ = nn($1, 's', $1, $4);
 392                                   $$->val=0; trackchanuse($4, ZN, 'S');
 393                                   any_runs($4);
 394                                 }
 395         | IF options FI         { $$ = nn($1, IF, ZN, ZN);
 396                                   $$->sl = $2->sl;
 397                                   prune_opts($$);
 398                                 }
 399         | DO                    { pushbreak(); }
 400           options OD            { $$ = nn($1, DO, ZN, ZN);
 401                                   $$->sl = $3->sl;
 402                                   prune_opts($$);
 403                                 }
 404         | BREAK                 { $$ = nn(ZN, GOTO, ZN, ZN);
 405                                   $$->sym = break_dest();
 406                                 }
 407         | GOTO NAME             { $$ = nn($2, GOTO, ZN, ZN);
 408                                   if ($2->sym->type != 0
 409                                   &&  $2->sym->type != LABEL) {
 410                                         non_fatal("bad label-name %s",
 411                                         $2->sym->name);
 412                                   }
 413                                   $2->sym->type = LABEL;
 414                                 }
 415         | NAME ':' stmnt        { $$ = nn($1, ':',$3, ZN);
 416                                   if ($1->sym->type != 0
 417                                   &&  $1->sym->type != LABEL) {
 418                                         non_fatal("bad label-name %s",
 419                                         $1->sym->name);
 420                                   }
 421                                   $1->sym->type = LABEL;
 422                                 }
 423         ;
 424
 425 Stmnt   : varref ASGN expr      { $$ = nn($1, ASGN, $1, $3);
 426                                   trackvar($1, $3);
 427                                   nochan_manip($1, $3, 0);
 428                                   no_internals($1);
 429                                 }
 430         | varref INCR           { $$ = nn(ZN,CONST, ZN, ZN); $$->val = 1;
 431                                   $$ = nn(ZN,  '+', $1, $$);
 432                                   $$ = nn($1, ASGN, $1, $$);
 433                                   trackvar($1, $1);
 434                                   no_internals($1);
 435                                   if ($1->sym->type == CHAN)
 436                                    fatal("arithmetic on chan", (char *)0);
 437                                 }
 438         | varref DECR           { $$ = nn(ZN,CONST, ZN, ZN); $$->val = 1;
 439                                   $$ = nn(ZN,  '-', $1, $$);
 440                                   $$ = nn($1, ASGN, $1, $$);
 441                                   trackvar($1, $1);
 442                                   no_internals($1);
 443                                   if ($1->sym->type == CHAN)
 444                                    fatal("arithmetic on chan id's", (char *)0);
 445                                 }
 446         | PRINT '(' STRING      { realread = 0; }
 447           prargs ')'            { $$ = nn($3, PRINT, $5, ZN); realread = 1; }
 448         | PRINTM '(' varref ')' { $$ = nn(ZN, PRINTM, $3, ZN); }
 449         | PRINTM '(' CONST ')'  { $$ = nn(ZN, PRINTM, $3, ZN); }
 450         | ASSERT full_expr      { $$ = nn(ZN, ASSERT, $2, ZN); AST_track($2, 0); }
 451         | ccode                 { $$ = $1; }
 452         | varref R_RCV          { Expand_Ok++; }
 453           rargs                 { Expand_Ok--; has_io++;
 454                                   $$ = nn($1,  'r', $1, $4);
 455                                   $$->val = has_random = 1;
 456                                   trackchanuse($4, ZN, 'R');
 457                                 }
 458         | varref RCV            { Expand_Ok++; }
 459           LT rargs GT           { Expand_Ok--; has_io++;
 460                                   $$ = nn($1, 'r', $1, $5);
 461                                   $$->val = 2;  /* fifo poll */
 462                                   trackchanuse($5, ZN, 'R');
 463                                 }
 464         | varref R_RCV          { Expand_Ok++; }
 465           LT rargs GT           { Expand_Ok--; has_io++;        /* rrcv poll */
 466                                   $$ = nn($1, 'r', $1, $5);
 467                                   $$->val = 3; has_random = 1;
 468                                   trackchanuse($5, ZN, 'R');
 469                                 }
 470         | varref O_SND          { Expand_Ok++; }
 471           margs                 { Expand_Ok--; has_io++;
 472                                   $$ = nn($1, 's', $1, $4);
 473                                   $$->val = has_sorted = 1;
 474                                   trackchanuse($4, ZN, 'S');
 475                                   any_runs($4);
 476                                 }
 477         | full_expr             { $$ = nn(ZN, 'c', $1, ZN); count_runs($$); }
 478         | ELSE                  { $$ = nn(ZN,ELSE,ZN,ZN);
 479                                 }
 480         | ATOMIC   '{'          { open_seq(0); }
 481           sequence OS '}'       { $$ = nn($1, ATOMIC, ZN, ZN);
 482                                   $$->sl = seqlist(close_seq(3), 0);
 483                                   make_atomic($$->sl->this, 0);
 484                                 }
 485         | D_STEP '{'            { open_seq(0); rem_Seq(); }
 486           sequence OS '}'       { $$ = nn($1, D_STEP, ZN, ZN);
 487                                   $$->sl = seqlist(close_seq(4), 0);
 488                                   make_atomic($$->sl->this, D_ATOM);
 489                                   unrem_Seq();
 490                                 }
 491         | '{'                   { open_seq(0); }
 492           sequence OS '}'       { $$ = nn(ZN, NON_ATOMIC, ZN, ZN);
 493                                   $$->sl = seqlist(close_seq(5), 0);
 494                                 }
 495         | INAME                 { IArgs++; }
 496           '(' args ')'          { pickup_inline($1->sym, $4); IArgs--; }
 497           Stmnt                 { $$ = $7; }
 498         ;
 499
 500 options : option                { $$->sl = seqlist($1->sq, 0); }
 501         | option options        { $$->sl = seqlist($1->sq, $2->sl); }
 502         ;
 503
 504 option  : SEP                   { open_seq(0); }
 505           sequence OS           { $$ = nn(ZN,0,ZN,ZN);
 506                                   $$->sq = close_seq(6); }
 507         ;
 508
 509 OS      : /* empty */
 510         | SEMI                  { /* redundant semi at end of sequence */ }
 511         ;
 512
 513 MS      : SEMI                  { /* at least one semi-colon */ }
 514         | MS SEMI               { /* but more are okay too   */ }
 515         ;
 516
 517 aname   : NAME                  { $$ = $1; }
 518         | PNAME                 { $$ = $1; }
 519         ;
 520
 521 expr    : '(' expr ')'          { $$ = $2; }
 522         | expr '+' expr         { $$ = nn(ZN, '+', $1, $3); }
 523         | expr '-' expr         { $$ = nn(ZN, '-', $1, $3); }
 524         | expr '*' expr         { $$ = nn(ZN, '*', $1, $3); }
 525         | expr '/' expr         { $$ = nn(ZN, '/', $1, $3); }
 526         | expr '%' expr         { $$ = nn(ZN, '%', $1, $3); }
 527         | expr '&' expr         { $$ = nn(ZN, '&', $1, $3); }
 528         | expr '^' expr         { $$ = nn(ZN, '^', $1, $3); }
 529         | expr '|' expr         { $$ = nn(ZN, '|', $1, $3); }
 530         | expr GT expr          { $$ = nn(ZN,  GT, $1, $3); }
 531         | expr LT expr          { $$ = nn(ZN,  LT, $1, $3); }
 532         | expr GE expr          { $$ = nn(ZN,  GE, $1, $3); }
 533         | expr LE expr          { $$ = nn(ZN,  LE, $1, $3); }
 534         | expr EQ expr          { $$ = nn(ZN,  EQ, $1, $3); }
 535         | expr NE expr          { $$ = nn(ZN,  NE, $1, $3); }
 536         | expr AND expr         { $$ = nn(ZN, AND, $1, $3); }
 537         | expr OR  expr         { $$ = nn(ZN,  OR, $1, $3); }
 538         | expr LSHIFT expr      { $$ = nn(ZN, LSHIFT,$1, $3); }
 539         | expr RSHIFT expr      { $$ = nn(ZN, RSHIFT,$1, $3); }
 540         | '~' expr              { $$ = nn(ZN, '~', $2, ZN); }
 541         | '-' expr %prec UMIN   { $$ = nn(ZN, UMIN, $2, ZN); }
 542         | SND expr %prec NEG    { $$ = nn(ZN, '!', $2, ZN); }
 543
 544         | '(' expr SEMI expr ':' expr ')' {
 545                                   $$ = nn(ZN,  OR, $4, $6);
 546                                   $$ = nn(ZN, '?', $2, $$);
 547                                 }
 548
 549         | RUN aname             { Expand_Ok++;
 550                                   if (!context)
 551                                   fatal("used 'run' outside proctype",
 552                                         (char *) 0);
 553                                   if (strcmp(context->name, ":init:") != 0)
 554                                         runsafe = 0;
 555                                 }
 556           '(' args ')'
 557           Opt_priority          { Expand_Ok--;
 558                                   $$ = nn($2, RUN, $5, ZN);
 559                                   $$->val = ($7) ? $7->val : 1;
 560                                   trackchanuse($5, $2, 'A'); trackrun($$);
 561                                 }
 562         | LEN '(' varref ')'    { $$ = nn($3, LEN, $3, ZN); }
 563         | ENABLED '(' expr ')'  { $$ = nn(ZN, ENABLED, $3, ZN);
 564                                   has_enabled++;
 565                                 }
 566         | varref RCV            { Expand_Ok++; }
 567           '[' rargs ']'         { Expand_Ok--; has_io++;
 568                                   $$ = nn($1, 'R', $1, $5);
 569                                 }
 570         | varref R_RCV          { Expand_Ok++; }
 571           '[' rargs ']'         { Expand_Ok--; has_io++;
 572                                   $$ = nn($1, 'R', $1, $5);
 573                                   $$->val = has_random = 1;
 574                                 }
 575         | varref                { $$ = $1; trapwonly($1, "varref"); }
 576         | cexpr                 { $$ = $1; }
 577         | CONST                 { $$ = nn(ZN,CONST,ZN,ZN);
 578                                   $$->ismtyp = $1->ismtyp;
 579                                   $$->val = $1->val;
 580                                 }
 581         | TIMEOUT               { $$ = nn(ZN,TIMEOUT, ZN, ZN); }
 582         | NONPROGRESS           { $$ = nn(ZN,NONPROGRESS, ZN, ZN);
 583                                   has_np++;
 584                                 }
 585         | PC_VAL '(' expr ')'   { $$ = nn(ZN, PC_VAL, $3, ZN);
 586                                   has_pcvalue++;
 587                                 }
 588         | PNAME '[' expr ']' '@' NAME
 589                                 { $$ = rem_lab($1->sym, $3, $6->sym); }
 590         | PNAME '[' expr ']' ':' pfld
 591                                 { $$ = rem_var($1->sym, $3, $6->sym, $6->lft); }
 592         | PNAME '@' NAME        { $$ = rem_lab($1->sym, ZN, $3->sym); }
 593         | PNAME ':' pfld        { $$ = rem_var($1->sym, ZN, $3->sym, $3->lft); }
 594         ;
 595
 596 Opt_priority:   /* none */      { $$ = ZN; }
 597         | PRIORITY CONST        { $$ = $2; }
 598         ;
 599
 600 full_expr:      expr            { $$ = $1; }
 601         |       Expr            { $$ = $1; }
 602         ;
 603
 604 Opt_enabler:    /* none */      { $$ = ZN; }
 605         | PROVIDED '(' full_expr ')'    { if (!proper_enabler($3))
 606                                   {     non_fatal("invalid PROVIDED clause",
 607                                                 (char *)0);
 608                                         $$ = ZN;
 609                                   } else
 610                                         $$ = $3;
 611                                  }
 612         | PROVIDED error        { $$ = ZN;
 613                                   non_fatal("usage: provided ( ..expr.. )",
 614                                         (char *)0);
 615                                 }
 616         ;
 617
 618         /* an Expr cannot be negated - to protect Probe expressions */
 619 Expr    : Probe                 { $$ = $1; }
 620         | '(' Expr ')'          { $$ = $2; }
 621         | Expr AND Expr         { $$ = nn(ZN, AND, $1, $3); }
 622         | Expr AND expr         { $$ = nn(ZN, AND, $1, $3); }
 623         | Expr OR  Expr         { $$ = nn(ZN,  OR, $1, $3); }
 624         | Expr OR  expr         { $$ = nn(ZN,  OR, $1, $3); }
 625         | expr AND Expr         { $$ = nn(ZN, AND, $1, $3); }
 626         | expr OR  Expr         { $$ = nn(ZN,  OR, $1, $3); }
 627         ;
 628
 629 Probe   : FULL '(' varref ')'   { $$ = nn($3,  FULL, $3, ZN); }
 630         | NFULL '(' varref ')'  { $$ = nn($3, NFULL, $3, ZN); }
 631         | EMPTY '(' varref ')'  { $$ = nn($3, EMPTY, $3, ZN); }
 632         | NEMPTY '(' varref ')' { $$ = nn($3,NEMPTY, $3, ZN); }
 633         ;
 634
 635 basetype: TYPE                  { $$->sym = ZS;
 636                                   $$->val = $1->val;
 637                                   if ($$->val == UNSIGNED)
 638                                   fatal("unsigned cannot be used as mesg type", 0);
 639                                 }
 640         | UNAME                 { $$->sym = $1->sym;
 641                                   $$->val = STRUCT;
 642                                 }
 643         | error                 /* e.g., unsigned ':' const */
 644         ;
 645
 646 typ_list: basetype              { $$ = nn($1, $1->val, ZN, ZN); }
 647         | basetype ',' typ_list { $$ = nn($1, $1->val, ZN, $3); }
 648         ;
 649
 650 args    : /* empty */           { $$ = ZN; }
 651         | arg                   { $$ = $1; }
 652         ;
 653
 654 prargs  : /* empty */           { $$ = ZN; }
 655         | ',' arg               { $$ = $2; }
 656         ;
 657
 658 margs   : arg                   { $$ = $1; }
 659         | expr '(' arg ')'      { if ($1->ntyp == ',')
 660                                         $$ = tail_add($1, $3);
 661                                   else
 662                                         $$ = nn(ZN, ',', $1, $3);
 663                                 }
 664         ;
 665
 666 arg     : expr                  { if ($1->ntyp == ',')
 667                                         $$ = $1;
 668                                   else
 669                                         $$ = nn(ZN, ',', $1, ZN);
 670                                 }
 671         | expr ',' arg          { if ($1->ntyp == ',')
 672                                         $$ = tail_add($1, $3);
 673                                   else
 674                                         $$ = nn(ZN, ',', $1, $3);
 675                                 }
 676         ;
 677
 678 rarg    : varref                { $$ = $1; trackvar($1, $1);
 679                                   trapwonly($1, "rarg"); }
 680         | EVAL '(' expr ')'     { $$ = nn(ZN,EVAL,$3,ZN);
 681                                   trapwonly($1, "eval rarg"); }
 682         | CONST                 { $$ = nn(ZN,CONST,ZN,ZN);
 683                                   $$->ismtyp = $1->ismtyp;
 684                                   $$->val = $1->val;
 685                                 }
 686         | '-' CONST %prec UMIN  { $$ = nn(ZN,CONST,ZN,ZN);
 687                                   $$->val = - ($2->val);
 688                                 }
 689         ;
 690
 691 rargs   : rarg                  { if ($1->ntyp == ',')
 692                                         $$ = $1;
 693                                   else
 694                                         $$ = nn(ZN, ',', $1, ZN);
 695                                 }
 696         | rarg ',' rargs        { if ($1->ntyp == ',')
 697                                         $$ = tail_add($1, $3);
 698                                   else
 699                                         $$ = nn(ZN, ',', $1, $3);
 700                                 }
 701         | rarg '(' rargs ')'    { if ($1->ntyp == ',')
 702                                         $$ = tail_add($1, $3);
 703                                   else
 704                                         $$ = nn(ZN, ',', $1, $3);
 705                                 }
 706         | '(' rargs ')'         { $$ = $2; }
 707         ;
 708
 709 nlst    : NAME                  { $$ = nn($1, NAME, ZN, ZN);
 710                                   $$ = nn(ZN, ',', $$, ZN); }
 711         | nlst NAME             { $$ = nn($2, NAME, ZN, ZN);
 712                                   $$ = nn(ZN, ',', $$, $1);
 713                                 }
 714         | nlst ','              { $$ = $1; /* commas optional */ }
 715         ;
 716 %%
 717
 718 void
 719 yyerror(char *fmt, ...)
 720 {
 721         non_fatal(fmt, (char *) 0);
 722 }