sys/src/cmd/spin/spin.y

   1 /***** spin: spin.y *****/
   2
   3 /*
   4  * This file is part of the public release of Spin. It is subject to the
   5  * terms in the LICENSE file that is included in this source directory.
   6  * Tool documentation is available at http://spinroot.com
   7  */
   8
   9 %{
  10 #include "spin.h"
  11 #include <sys/types.h>
  12 #ifndef PC
  13 #include <unistd.h>
  14 #endif
  15 #include <stdarg.h>
  16
  17 #define YYMAXDEPTH      20000   /* default is 10000 */
  18 #define YYDEBUG         0
  19 #define Stop    nn(ZN,'@',ZN,ZN)
  20 #define PART0   "place initialized declaration of "
  21 #define PART1   "place initialized chan decl of "
  22 #define PART2   " at start of proctype "
  23
  24 static  Lextok *ltl_to_string(Lextok *);
  25
  26 extern  Symbol  *context, *owner;
  27 extern  Lextok *for_body(Lextok *, int);
  28 extern  void for_setup(Lextok *, Lextok *, Lextok *);
  29 extern  Lextok *for_index(Lextok *, Lextok *);
  30 extern  Lextok *sel_index(Lextok *, Lextok *, Lextok *);
  31 extern  void    keep_track_off(Lextok *);
  32 extern  void    safe_break(void);
  33 extern  void    restore_break(void);
  34 extern  int     u_sync, u_async, dumptab, scope_level;
  35 extern  int     initialization_ok;
  36 extern  short   has_sorted, has_random, has_enabled, has_pcvalue, has_np, has_priority;
  37 extern  short   has_code, has_state, has_ltl, has_io;
  38 extern  void    count_runs(Lextok *);
  39 extern  void    no_internals(Lextok *);
  40 extern  void    any_runs(Lextok *);
  41 extern  void    explain(int);
  42 extern  void    ltl_list(char *, char *);
  43 extern  void    validref(Lextok *, Lextok *);
  44 extern  void    sanity_check(Lextok *);
  45 extern  char    yytext[];
  46
  47 int     Mpars = 0;      /* max nr of message parameters  */
  48 int     nclaims = 0;    /* nr of never claims */
  49 int     ltl_mode = 0;   /* set when parsing an ltl formula */
  50 int     Expand_Ok = 0, realread = 1, IArgs = 0, NamesNotAdded = 0;
  51 int     in_for = 0, in_seq = 0, par_cnt = 0;
  52 int     dont_simplify = 0;
  53 char    *claimproc = (char *) 0;
  54 char    *eventmap = (char *) 0;
  55
  56 static  char *ltl_name;
  57 static  int  Embedded = 0, inEventMap = 0, has_ini = 0;
  58
  59 %}
  60
  61 %token  ASSERT PRINT PRINTM PREPROC
  62 %token  C_CODE C_DECL C_EXPR C_STATE C_TRACK
  63 %token  RUN LEN ENABLED SET_P GET_P EVAL PC_VAL
  64 %token  TYPEDEF MTYPE INLINE RETURN LABEL OF
  65 %token  GOTO BREAK ELSE SEMI ARROW
  66 %token  IF FI DO OD FOR SELECT IN SEP DOTDOT
  67 %token  ATOMIC NON_ATOMIC D_STEP UNLESS
  68 %token  TIMEOUT NONPROGRESS
  69 %token  ACTIVE PROCTYPE D_PROCTYPE
  70 %token  HIDDEN SHOW ISLOCAL
  71 %token  PRIORITY PROVIDED
  72 %token  FULL EMPTY NFULL NEMPTY
  73 %token  CONST TYPE XU                   /* val */
  74 %token  NAME UNAME PNAME INAME          /* sym */
  75 %token  STRING CLAIM TRACE INIT LTL     /* sym */
  76
  77 %right  ASGN
  78 %left   SND O_SND RCV R_RCV /* SND doubles as boolean negation */
  79 %left   IMPLIES EQUIV                   /* ltl */
  80 %left   OR
  81 %left   AND
  82 %left   ALWAYS EVENTUALLY               /* ltl */
  83 %left   UNTIL WEAK_UNTIL RELEASE        /* ltl */
  84 %right  NEXT                            /* ltl */
  85 %left   '|'
  86 %left   '^'
  87 %left   '&'
  88 %left   EQ NE
  89 %left   GT LT GE LE
  90 %left   LSHIFT RSHIFT
  91 %left   '+' '-'
  92 %left   '*' '/' '%'
  93 %left   INCR DECR
  94 %right  '~' UMIN NEG
  95 %left   DOT
  96 %%
  97
  98 /** PROMELA Grammar Rules **/
  99
 100 program : units         { yytext[0] = '\0'; }
 101         ;
 102
 103 units   : unit
 104         | units unit
 105         ;
 106
 107 unit    : proc          /* proctype { }       */
 108         | init          /* init { }           */
 109         | claim         /* never claim        */
 110         | ltl           /* ltl formula        */
 111         | events        /* event assertions   */
 112         | one_decl      /* variables, chans   */
 113         | utype         /* user defined types */
 114         | c_fcts        /* c functions etc.   */
 115         | ns            /* named sequence     */
 116         | semi          /* optional separator */
 117         | error
 118         ;
 119
 120 l_par   : '('           { par_cnt++; }
 121         ;
 122
 123 r_par   : ')'           { par_cnt--; }
 124         ;
 125
 126
 127 proc    : inst          /* optional instantiator */
 128           proctype NAME {
 129                           setptype($3, PROCTYPE, ZN);
 130                           setpname($3);
 131                           context = $3->sym;
 132                           context->ini = $2; /* linenr and file */
 133                           Expand_Ok++; /* expand struct names in decl */
 134                           has_ini = 0;
 135                         }
 136           l_par decl r_par      { Expand_Ok--;
 137                           if (has_ini)
 138                           fatal("initializer in parameter list", (char *) 0);
 139                         }
 140           Opt_priority
 141           Opt_enabler
 142           body          { ProcList *rl;
 143                           if ($1 != ZN && $1->val > 0)
 144                           {     int j;
 145                                 rl = ready($3->sym, $6, $11->sq, $2->val, $10, A_PROC);
 146                                 for (j = 0; j < $1->val; j++)
 147                                 {       runnable(rl, $9?$9->val:1, 1);
 148                                 announce(":root:");
 149                                 }
 150                                 if (dumptab) $3->sym->ini = $1;
 151                           } else
 152                           {     rl = ready($3->sym, $6, $11->sq, $2->val, $10, P_PROC);
 153                           }
 154                           if (rl && has_ini == 1)       /* global initializations, unsafe */
 155                           {     /* printf("proctype %s has initialized data\n",
 156                                         $3->sym->name);
 157                                  */
 158                                 rl->unsafe = 1;
 159                           }
 160                           context = ZS;
 161                         }
 162         ;
 163
 164 proctype: PROCTYPE      { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 0; }
 165         | D_PROCTYPE    { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 1; }
 166         ;
 167
 168 inst    : /* empty */   { $$ = ZN; }
 169         | ACTIVE        { $$ = nn(ZN,CONST,ZN,ZN); $$->val = 1; }
 170         | ACTIVE '[' const_expr ']' {
 171                           $$ = nn(ZN,CONST,ZN,ZN); $$->val = $3->val;
 172                           if ($3->val > 255)
 173                                 non_fatal("max nr of processes is 255\n", "");
 174                         }
 175         | ACTIVE '[' NAME ']' {
 176                           $$ = nn(ZN,CONST,ZN,ZN);
 177                           $$->val = 0;
 178                           if (!$3->sym->type)
 179                                 fatal("undeclared variable %s",
 180                                         $3->sym->name);
 181                           else if ($3->sym->ini->ntyp != CONST)
 182                                 fatal("need constant initializer for %s\n",
 183                                         $3->sym->name);
 184                           else
 185                                 $$->val = $3->sym->ini->val;
 186                         }
 187         ;
 188
 189 init    : INIT          { context = $1->sym; }
 190           Opt_priority
 191           body          { ProcList *rl;
 192                           rl = ready(context, ZN, $4->sq, 0, ZN, I_PROC);
 193                           runnable(rl, $3?$3->val:1, 1);
 194                           announce(":root:");
 195                           context = ZS;
 196                         }
 197         ;
 198
 199 ltl     : LTL optname2  { ltl_mode = 1; ltl_name = $2->sym->name; }
 200           ltl_body      { if ($4) ltl_list($2->sym->name, $4->sym->name);
 201                           ltl_mode = 0; has_ltl = 1;
 202                         }
 203         ;
 204
 205 ltl_body: '{' full_expr OS '}' { $$ = ltl_to_string($2); }
 206         | error         { $$ = NULL; }
 207         ;
 208
 209 claim   : CLAIM optname { if ($2 != ZN)
 210                           {     $1->sym = $2->sym;      /* new 5.3.0 */
 211                           }
 212                           nclaims++;
 213                           context = $1->sym;
 214                           if (claimproc && !strcmp(claimproc, $1->sym->name))
 215                           {     fatal("claim %s redefined", claimproc);
 216                           }
 217                           claimproc = $1->sym->name;
 218                         }
 219           body          { (void) ready($1->sym, ZN, $4->sq, 0, ZN, N_CLAIM);
 220                           context = ZS;
 221                         }
 222         ;
 223
 224 optname : /* empty */   { char tb[32];
 225                           memset(tb, 0, 32);
 226                           sprintf(tb, "never_%d", nclaims);
 227                           $$ = nn(ZN, NAME, ZN, ZN);
 228                           $$->sym = lookup(tb);
 229                         }
 230         | NAME          { $$ = $1; }
 231         ;
 232
 233 optname2 : /* empty */ { char tb[32]; static int nltl = 0;
 234                           memset(tb, 0, 32);
 235                           sprintf(tb, "ltl_%d", nltl++);
 236                           $$ = nn(ZN, NAME, ZN, ZN);
 237                           $$->sym = lookup(tb);
 238                         }
 239         | NAME          { $$ = $1; }
 240         ;
 241
 242 events : TRACE          { context = $1->sym;
 243                           if (eventmap)
 244                                 non_fatal("trace %s redefined", eventmap);
 245                           eventmap = $1->sym->name;
 246                           inEventMap++;
 247                         }
 248           body          {
 249                           if (strcmp($1->sym->name, ":trace:") == 0)
 250                           {     (void) ready($1->sym, ZN, $3->sq, 0, ZN, E_TRACE);
 251                           } else
 252                           {     (void) ready($1->sym, ZN, $3->sq, 0, ZN, N_TRACE);
 253                           }
 254                           context = ZS;
 255                           inEventMap--;
 256                         }
 257         ;
 258
 259 utype   : TYPEDEF NAME '{'      {  if (context)
 260                                    { fatal("typedef %s must be global",
 261                                         $2->sym->name);
 262                                    }
 263                                    owner = $2->sym;
 264                                    in_seq = $1->ln;
 265                                 }
 266           decl_lst '}'          { setuname($5);
 267                                   owner = ZS;
 268                                   in_seq = 0;
 269                                 }
 270         ;
 271
 272 nm      : NAME                  { $$ = $1; }
 273         | INAME                 { $$ = $1;
 274                                   if (IArgs)
 275                                   fatal("invalid use of '%s'", $1->sym->name);
 276                                 }
 277         ;
 278
 279 ns      : INLINE nm l_par               { NamesNotAdded++; }
 280           args r_par            { prep_inline($2->sym, $5);
 281                                   NamesNotAdded--;
 282                                 }
 283         ;
 284
 285 c_fcts  : ccode                 { /* leaves pseudo-inlines with sym of
 286                                    * type CODE_FRAG or CODE_DECL in global context
 287                                    */
 288                                 }
 289         | cstate
 290         ;
 291
 292 cstate  : C_STATE STRING STRING {
 293                                   c_state($2->sym, $3->sym, ZS);
 294                                   has_code = has_state = 1;
 295                                 }
 296         | C_TRACK STRING STRING {
 297                                   c_track($2->sym, $3->sym, ZS);
 298                                   has_code = has_state = 1;
 299                                 }
 300         | C_STATE STRING STRING STRING {
 301                                   c_state($2->sym, $3->sym, $4->sym);
 302                                   has_code = has_state = 1;
 303                                 }
 304         | C_TRACK STRING STRING STRING {
 305                                   c_track($2->sym, $3->sym, $4->sym);
 306                                   has_code = has_state = 1;
 307                                 }
 308         ;
 309
 310 ccode   : C_CODE                { Symbol *s;
 311                                   NamesNotAdded++;
 312                                   s = prep_inline(ZS, ZN);
 313                                   NamesNotAdded--;
 314                                   $$ = nn(ZN, C_CODE, ZN, ZN);
 315                                   $$->sym = s;
 316                                   $$->ln = $1->ln;
 317                                   $$->fn = $1->fn;
 318                                   has_code = 1;
 319                                 }
 320         | C_DECL                { Symbol *s;
 321                                   NamesNotAdded++;
 322                                   s = prep_inline(ZS, ZN);
 323                                   NamesNotAdded--;
 324                                   s->type = CODE_DECL;
 325                                   $$ = nn(ZN, C_CODE, ZN, ZN);
 326                                   $$->sym = s;
 327                                   $$->ln = $1->ln;
 328                                   $$->fn = $1->fn;
 329                                   has_code = 1;
 330                                 }
 331         ;
 332 cexpr   : C_EXPR                { Symbol *s;
 333                                   NamesNotAdded++;
 334                                   s = prep_inline(ZS, ZN);
 335 /* if context is 0 this was inside an ltl formula
 336    mark the last inline added to seqnames */
 337                                   if (!context)
 338                                   {     mark_last();
 339                                   }
 340                                   NamesNotAdded--;
 341                                   $$ = nn(ZN, C_EXPR, ZN, ZN);
 342                                   $$->sym = s;
 343                                   $$->ln = $1->ln;
 344                                   $$->fn = $1->fn;
 345                                   no_side_effects(s->name);
 346                                   has_code = 1;
 347                                 }
 348         ;
 349
 350 body    : '{'                   { open_seq(1); in_seq = $1->ln; }
 351           sequence OS           { add_seq(Stop); }
 352           '}'                   { $$->sq = close_seq(0); in_seq = 0;
 353                                   if (scope_level != 0)
 354                                   {     non_fatal("missing '}' ?", 0);
 355                                         scope_level = 0;
 356                                   }
 357                                 }
 358         ;
 359
 360 sequence: step                  { if ($1) add_seq($1); }
 361         | sequence MS step      { if ($3) add_seq($3); }
 362         ;
 363
 364 step    : one_decl              { $$ = ZN; }
 365         | XU vref_lst           { setxus($2, $1->val); $$ = ZN; }
 366         | NAME ':' one_decl     { fatal("label preceding declaration,", (char *)0); }
 367         | NAME ':' XU           { fatal("label predecing xr/xs claim,", 0); }
 368         | stmnt                 { $$ = $1; }
 369         | stmnt UNLESS          { if ($1->ntyp == DO) { safe_break(); } }
 370           stmnt                 { if ($1->ntyp == DO) { restore_break(); }
 371                                   $$ = do_unless($1, $4);
 372                                 }
 373         | error                 { printf("Not a Step\n"); }
 374         ;
 375
 376 vis     : /* empty */           { $$ = ZN; }
 377         | HIDDEN                { $$ = $1; }
 378         | SHOW                  { $$ = $1; }
 379         | ISLOCAL               { $$ = $1; }
 380         ;
 381
 382 asgn:   /* empty */
 383         | ASGN
 384         ;
 385
 386 one_decl: vis TYPE var_list     { setptype($3, $2->val, $1);
 387                                   $$ = $3;
 388                                 }
 389         | vis UNAME var_list    { setutype($3, $2->sym, $1);
 390                                   $$ = expand($3, Expand_Ok);
 391                                 }
 392         | vis TYPE asgn '{' nlst '}' {
 393                                   if ($2->val != MTYPE)
 394                                         fatal("malformed declaration", 0);
 395                                   setmtype($5);
 396                                   if ($1)
 397                                         non_fatal("cannot %s mtype (ignored)",
 398                                                 $1->sym->name);
 399                                   if (context != ZS)
 400                                         fatal("mtype declaration must be global", 0);
 401                                 }
 402         ;
 403
 404 decl_lst: one_decl              { $$ = nn(ZN, ',', $1, ZN); }
 405         | one_decl SEMI
 406           decl_lst              { $$ = nn(ZN, ',', $1, $3); }
 407         ;
 408
 409 decl    : /* empty */           { $$ = ZN; }
 410         | decl_lst              { $$ = $1; }
 411         ;
 412
 413 vref_lst: varref                { $$ = nn($1, XU, $1, ZN); }
 414         | varref ',' vref_lst   { $$ = nn($1, XU, $1, $3); }
 415         ;
 416
 417 var_list: ivar                  { $$ = nn($1, TYPE, ZN, ZN); }
 418         | ivar ',' var_list     { $$ = nn($1, TYPE, ZN, $3); }
 419         ;
 420
 421 c_list  : CONST                 { $1->ntyp = CONST; $$ = $1; }
 422         | CONST ',' c_list      { $1->ntyp = CONST; $$ = nn($1, ',', $1, $3); }
 423         ;
 424
 425 ivar    : vardcl                { $$ = $1;
 426                                   $1->sym->ini = nn(ZN,CONST,ZN,ZN);
 427                                   $1->sym->ini->val = 0;
 428                                   if (!initialization_ok)
 429                                   {     Lextok *zx, *xz;
 430                                         zx = nn(ZN, NAME, ZN, ZN);
 431                                         zx->sym = $1->sym;
 432                                         xz = nn(zx, ASGN, zx, $1->sym->ini);
 433                                         keep_track_off(xz);
 434                                         /* make sure zx doesnt turn out to be a STRUCT later */
 435                                         add_seq(xz);
 436                                   }
 437                                 }
 438         | vardcl ASGN '{' c_list '}'    {
 439                                   if (!$1->sym->isarray)
 440                                         fatal("%s must be an array", $1->sym->name);
 441                                   $$ = $1;
 442                                   $1->sym->ini = $4;
 443                                   has_ini = 1;
 444                                   $1->sym->hidden |= (4|8);     /* conservative */
 445                                   if (!initialization_ok)
 446                                   {     Lextok *zx = nn(ZN, NAME, ZN, ZN);
 447                                         zx->sym = $1->sym;
 448                                         add_seq(nn(zx, ASGN, zx, $4));
 449                                   }
 450                                 }
 451         | vardcl ASGN expr      { $$ = $1;
 452                                   $1->sym->ini = $3;
 453                                   if ($3->ntyp == CONST
 454                                   || ($3->ntyp == NAME && $3->sym->context))
 455                                   {     has_ini = 2; /* local init */
 456                                   } else
 457                                   {     has_ini = 1; /* possibly global */
 458                                   }
 459                                   trackvar($1, $3);
 460                                   if (any_oper($3, RUN))
 461                                   {     fatal("cannot use 'run' in var init, saw", (char *) 0);
 462                                   }
 463                                   nochan_manip($1, $3, 0);
 464                                   no_internals($1);
 465                                   if (!initialization_ok)
 466                                   {     Lextok *zx = nn(ZN, NAME, ZN, ZN);
 467                                         zx->sym = $1->sym;
 468                                         add_seq(nn(zx, ASGN, zx, $3));
 469                                   }
 470                                 }
 471         | vardcl ASGN ch_init   { $1->sym->ini = $3;
 472                                   $$ = $1; has_ini = 1;
 473                                   if (!initialization_ok)
 474                                   {     non_fatal(PART1 "'%s'" PART2, $1->sym->name);
 475                                   }
 476                                 }
 477         ;
 478
 479 ch_init : '[' const_expr ']' OF
 480           '{' typ_list '}'      { if ($2->val)
 481                                         u_async++;
 482                                   else
 483                                         u_sync++;
 484                                   {     int i = cnt_mpars($6);
 485                                         Mpars = max(Mpars, i);
 486                                   }
 487                                   $$ = nn(ZN, CHAN, ZN, $6);
 488                                   $$->val = $2->val;
 489                                   $$->ln = $1->ln;
 490                                   $$->fn = $1->fn;
 491                                 }
 492         ;
 493
 494 vardcl  : NAME                  { $1->sym->nel = 1; $$ = $1; }
 495         | NAME ':' CONST        { $1->sym->nbits = $3->val;
 496                                   if ($3->val >= 8*sizeof(long))
 497                                   {     non_fatal("width-field %s too large",
 498                                                 $1->sym->name);
 499                                         $3->val = 8*sizeof(long)-1;
 500                                   }
 501                                   $1->sym->nel = 1; $$ = $1;
 502                                 }
 503         | NAME '[' const_expr ']'       { $1->sym->nel = $3->val; $1->sym->isarray = 1; $$ = $1; }
 504         | NAME '[' NAME ']'     {       /* make an exception for an initialized scalars */
 505                                         $$ = nn(ZN, CONST, ZN, ZN);
 506                                         fprintf(stderr, "spin: %s:%d, warning: '%s' in array bound ",
 507                                                 $1->fn->name, $1->ln, $3->sym->name);
 508                                         if ($3->sym->ini->val > 0)
 509                                         {       fprintf(stderr, "evaluated as %d\n", $3->sym->ini->val);
 510                                                 $$->val = $3->sym->ini->val;
 511                                         } else
 512                                         {       fprintf(stderr, "evaluated as 8 by default (to avoid zero)\n");
 513                                                 $$->val = 8;
 514                                         }
 515                                         $1->sym->nel = $$->val;
 516                                         $1->sym->isarray = 1;
 517                                         $$ = $1;
 518                                 }
 519         ;
 520
 521 varref  : cmpnd                 { $$ = mk_explicit($1, Expand_Ok, NAME); }
 522         ;
 523
 524 pfld    : NAME                  { $$ = nn($1, NAME, ZN, ZN);
 525                                   if ($1->sym->isarray && !in_for)
 526                                   {     non_fatal("missing array index for '%s'",
 527                                                 $1->sym->name);
 528                                   }
 529                                 }
 530         | NAME                  { owner = ZS; }
 531           '[' expr ']'          { $$ = nn($1, NAME, $4, ZN); }
 532         ;
 533
 534 cmpnd   : pfld                  { Embedded++;
 535                                   if ($1->sym->type == STRUCT)
 536                                         owner = $1->sym->Snm;
 537                                 }
 538           sfld                  { $$ = $1; $$->rgt = $3;
 539                                   if ($3 && $1->sym->type != STRUCT)
 540                                         $1->sym->type = STRUCT;
 541                                   Embedded--;
 542                                   if (!Embedded && !NamesNotAdded
 543                                   &&  !$1->sym->type)
 544                                    fatal("undeclared variable: %s",
 545                                                 $1->sym->name);
 546                                   if ($3) validref($1, $3->lft);
 547                                   owner = ZS;
 548                                 }
 549         ;
 550
 551 sfld    : /* empty */           { $$ = ZN; }
 552         | '.' cmpnd %prec DOT   { $$ = nn(ZN, '.', $2, ZN); }
 553         ;
 554
 555 stmnt   : Special               { $$ = $1; initialization_ok = 0; }
 556         | Stmnt                 { $$ = $1; initialization_ok = 0;
 557                                   if (inEventMap) non_fatal("not an event", (char *)0);
 558                                 }
 559         ;
 560
 561 for_pre : FOR l_par             { in_for = 1; }
 562           varref                { trapwonly($4 /*, "for" */);
 563                                   pushbreak(); /* moved up */
 564                                   $$ = $4;
 565                                 }
 566         ;
 567
 568 for_post: '{' sequence OS '}' ;
 569
 570 Special : varref RCV            { Expand_Ok++; }
 571           rargs                 { Expand_Ok--; has_io++;
 572                                   $$ = nn($1,  'r', $1, $4);
 573                                   trackchanuse($4, ZN, 'R');
 574                                 }
 575         | varref SND            { Expand_Ok++; }
 576           margs                 { Expand_Ok--; has_io++;
 577                                   $$ = nn($1, 's', $1, $4);
 578                                   $$->val=0; trackchanuse($4, ZN, 'S');
 579                                   any_runs($4);
 580                                 }
 581         | for_pre ':' expr DOTDOT expr r_par    {
 582                                   for_setup($1, $3, $5); in_for = 0;
 583                                 }
 584           for_post              { $$ = for_body($1, 1);
 585                                 }
 586         | for_pre IN varref r_par       { $$ = for_index($1, $3); in_for = 0;
 587                                 }
 588           for_post              { $$ = for_body($5, 1);
 589                                 }
 590         | SELECT l_par varref ':' expr DOTDOT expr r_par {
 591                                   trapwonly($3 /*, "select" */);
 592                                   $$ = sel_index($3, $5, $7);
 593                                 }
 594         | IF options FI         { $$ = nn($1, IF, ZN, ZN);
 595                                   $$->sl = $2->sl;
 596                                   $$->ln = $1->ln;
 597                                   $$->fn = $1->fn;
 598                                   prune_opts($$);
 599                                 }
 600         | DO                    { pushbreak(); }
 601           options OD            { $$ = nn($1, DO, ZN, ZN);
 602                                   $$->sl = $3->sl;
 603                                   $$->ln = $1->ln;
 604                                   $$->fn = $1->fn;
 605                                   prune_opts($$);
 606                                 }
 607         | BREAK                 { $$ = nn(ZN, GOTO, ZN, ZN);
 608                                   $$->sym = break_dest();
 609                                 }
 610         | GOTO NAME             { $$ = nn($2, GOTO, ZN, ZN);
 611                                   if ($2->sym->type != 0
 612                                   &&  $2->sym->type != LABEL) {
 613                                         non_fatal("bad label-name %s",
 614                                         $2->sym->name);
 615                                   }
 616                                   $2->sym->type = LABEL;
 617                                 }
 618         | NAME ':' stmnt        { $$ = nn($1, ':',$3, ZN);
 619                                   if ($1->sym->type != 0
 620                                   &&  $1->sym->type != LABEL) {
 621                                         non_fatal("bad label-name %s",
 622                                         $1->sym->name);
 623                                   }
 624                                   $1->sym->type = LABEL;
 625                                 }
 626         | NAME ':'              { $$ = nn($1, ':',ZN,ZN);
 627                                   if ($1->sym->type != 0
 628                                   &&  $1->sym->type != LABEL) {
 629                                         non_fatal("bad label-name %s",
 630                                         $1->sym->name);
 631                                   }
 632                                   $$->lft = nn(ZN, 'c', nn(ZN,CONST,ZN,ZN), ZN);
 633                                   $$->lft->lft->val = 1; /* skip */
 634                                   $1->sym->type = LABEL;
 635                                 }
 636         | error                 { $$ = nn(ZN, 'c', nn(ZN,CONST,ZN,ZN), ZN);
 637                                   $$->lft->val = 1; /* skip */
 638                                 }
 639         ;
 640
 641 Stmnt   : varref ASGN full_expr { $$ = nn($1, ASGN, $1, $3);
 642                                   trackvar($1, $3);
 643                                   nochan_manip($1, $3, 0);
 644                                   no_internals($1);
 645                                 }
 646         | varref INCR           { $$ = nn(ZN,CONST, ZN, ZN); $$->val = 1;
 647                                   $$ = nn(ZN,  '+', $1, $$);
 648                                   $$ = nn($1, ASGN, $1, $$);
 649                                   trackvar($1, $1);
 650                                   no_internals($1);
 651                                   if ($1->sym->type == CHAN)
 652                                    fatal("arithmetic on chan", (char *)0);
 653                                 }
 654         | varref DECR           { $$ = nn(ZN,CONST, ZN, ZN); $$->val = 1;
 655                                   $$ = nn(ZN,  '-', $1, $$);
 656                                   $$ = nn($1, ASGN, $1, $$);
 657                                   trackvar($1, $1);
 658                                   no_internals($1);
 659                                   if ($1->sym->type == CHAN)
 660                                    fatal("arithmetic on chan id's", (char *)0);
 661                                 }
 662         | SET_P l_par two_args r_par    { $$ = nn(ZN, SET_P, $3, ZN); has_priority++; }
 663         | PRINT l_par STRING    { realread = 0; }
 664           prargs r_par          { $$ = nn($3, PRINT, $5, ZN); realread = 1; }
 665         | PRINTM l_par varref r_par     { $$ = nn(ZN, PRINTM, $3, ZN); }
 666         | PRINTM l_par CONST r_par      { $$ = nn(ZN, PRINTM, $3, ZN); }
 667         | ASSERT full_expr      { $$ = nn(ZN, ASSERT, $2, ZN); AST_track($2, 0); }
 668         | ccode                 { $$ = $1; }
 669         | varref R_RCV          { Expand_Ok++; }
 670           rargs                 { Expand_Ok--; has_io++;
 671                                   $$ = nn($1,  'r', $1, $4);
 672                                   $$->val = has_random = 1;
 673                                   trackchanuse($4, ZN, 'R');
 674                                 }
 675         | varref RCV            { Expand_Ok++; }
 676           LT rargs GT           { Expand_Ok--; has_io++;
 677                                   $$ = nn($1, 'r', $1, $5);
 678                                   $$->val = 2;  /* fifo poll */
 679                                   trackchanuse($5, ZN, 'R');
 680                                 }
 681         | varref R_RCV          { Expand_Ok++; }
 682           LT rargs GT           { Expand_Ok--; has_io++;        /* rrcv poll */
 683                                   $$ = nn($1, 'r', $1, $5);
 684                                   $$->val = 3; has_random = 1;
 685                                   trackchanuse($5, ZN, 'R');
 686                                 }
 687         | varref O_SND          { Expand_Ok++; }
 688           margs                 { Expand_Ok--; has_io++;
 689                                   $$ = nn($1, 's', $1, $4);
 690                                   $$->val = has_sorted = 1;
 691                                   trackchanuse($4, ZN, 'S');
 692                                   any_runs($4);
 693                                 }
 694         | full_expr             { $$ = nn(ZN, 'c', $1, ZN); count_runs($$); }
 695         | ELSE                  { $$ = nn(ZN,ELSE,ZN,ZN);
 696                                 }
 697         | ATOMIC   '{'          { open_seq(0); }
 698           sequence OS '}'       { $$ = nn($1, ATOMIC, ZN, ZN);
 699                                   $$->sl = seqlist(close_seq(3), 0);
 700                                   $$->ln = $1->ln;
 701                                   $$->fn = $1->fn;
 702                                   make_atomic($$->sl->this, 0);
 703                                 }
 704         | D_STEP '{'            { open_seq(0);
 705                                   rem_Seq();
 706                                 }
 707           sequence OS '}'       { $$ = nn($1, D_STEP, ZN, ZN);
 708                                   $$->sl = seqlist(close_seq(4), 0);
 709                                   $$->ln = $1->ln;
 710                                   $$->fn = $1->fn;
 711                                   make_atomic($$->sl->this, D_ATOM);
 712                                   unrem_Seq();
 713                                 }
 714         | '{'                   { open_seq(0); }
 715           sequence OS '}'       { $$ = nn(ZN, NON_ATOMIC, ZN, ZN);
 716                                   $$->sl = seqlist(close_seq(5), 0);
 717                                   $$->ln = $1->ln;
 718                                   $$->fn = $1->fn;
 719                                 }
 720         | INAME                 { IArgs++; }
 721           l_par args r_par      { initialization_ok = 0;
 722                                   pickup_inline($1->sym, $4, ZN);
 723                                   IArgs--;
 724                                 }
 725           Stmnt                 { $$ = $7; }
 726
 727         | varref ASGN INAME     { IArgs++; }
 728           l_par args r_par      { initialization_ok = 0;
 729                                   pickup_inline($3->sym, $6, $1);
 730                                   IArgs--;
 731                                 }
 732           Stmnt                 { $$ = $9; }
 733         | RETURN full_expr      { $$ = return_statement($2); }
 734         ;
 735
 736 options : option                { $$->sl = seqlist($1->sq, 0); }
 737         | option options        { $$->sl = seqlist($1->sq, $2->sl); }
 738         ;
 739
 740 option  : SEP                   { open_seq(0); }
 741           sequence OS           { $$ = nn(ZN,0,ZN,ZN);
 742                                   $$->sq = close_seq(6);
 743                                   $$->ln = $1->ln;
 744                                   $$->fn = $1->fn;
 745                                 }
 746         ;
 747
 748 OS      : /* empty */
 749         | semi                  { /* redundant semi at end of sequence */ }
 750         ;
 751
 752 semi    : SEMI
 753         | ARROW
 754         ;
 755
 756 MS      : semi                  { /* at least one semi-colon */ }
 757         | MS semi               { /* but more are okay too   */ }
 758         ;
 759
 760 aname   : NAME                  { $$ = $1; }
 761         | PNAME                 { $$ = $1; }
 762         ;
 763
 764 const_expr:     CONST                   { $$ = $1; }
 765         | '-' const_expr %prec UMIN     { $$ = $2; $$->val = -($2->val); }
 766         | l_par const_expr r_par                { $$ = $2; }
 767         | const_expr '+' const_expr     { $$ = $1; $$->val = $1->val + $3->val; }
 768         | const_expr '-' const_expr     { $$ = $1; $$->val = $1->val - $3->val; }
 769         | const_expr '*' const_expr     { $$ = $1; $$->val = $1->val * $3->val; }
 770         | const_expr '/' const_expr     { $$ = $1; $$->val = $1->val / $3->val; }
 771         | const_expr '%' const_expr     { $$ = $1; $$->val = $1->val % $3->val; }
 772         ;
 773
 774 expr    : l_par expr r_par              { $$ = $2; }
 775         | expr '+' expr         { $$ = nn(ZN, '+', $1, $3); }
 776         | expr '-' expr         { $$ = nn(ZN, '-', $1, $3); }
 777         | expr '*' expr         { $$ = nn(ZN, '*', $1, $3); }
 778         | expr '/' expr         { $$ = nn(ZN, '/', $1, $3); }
 779         | expr '%' expr         { $$ = nn(ZN, '%', $1, $3); }
 780         | expr '&' expr         { $$ = nn(ZN, '&', $1, $3); }
 781         | expr '^' expr         { $$ = nn(ZN, '^', $1, $3); }
 782         | expr '|' expr         { $$ = nn(ZN, '|', $1, $3); }
 783         | expr GT expr          { $$ = nn(ZN,  GT, $1, $3); }
 784         | expr LT expr          { $$ = nn(ZN,  LT, $1, $3); }
 785         | expr GE expr          { $$ = nn(ZN,  GE, $1, $3); }
 786         | expr LE expr          { $$ = nn(ZN,  LE, $1, $3); }
 787         | expr EQ expr          { $$ = nn(ZN,  EQ, $1, $3); }
 788         | expr NE expr          { $$ = nn(ZN,  NE, $1, $3); }
 789         | expr AND expr         { $$ = nn(ZN, AND, $1, $3); }
 790         | expr OR  expr         { $$ = nn(ZN,  OR, $1, $3); }
 791         | expr LSHIFT expr      { $$ = nn(ZN, LSHIFT,$1, $3); }
 792         | expr RSHIFT expr      { $$ = nn(ZN, RSHIFT,$1, $3); }
 793         | '~' expr              { $$ = nn(ZN, '~', $2, ZN); }
 794         | '-' expr %prec UMIN   { $$ = nn(ZN, UMIN, $2, ZN); }
 795         | SND expr %prec NEG    { $$ = nn(ZN, '!', $2, ZN); }
 796
 797         | l_par expr ARROW expr ':' expr r_par {
 798                                   $$ = nn(ZN,  OR, $4, $6);
 799                                   $$ = nn(ZN, '?', $2, $$);
 800                                 }
 801
 802         | RUN aname             { Expand_Ok++;
 803                                   if (!context)
 804                                    fatal("used 'run' outside proctype",
 805                                         (char *) 0);
 806                                 }
 807           l_par args r_par
 808           Opt_priority          { Expand_Ok--;
 809                                   $$ = nn($2, RUN, $5, ZN);
 810                                   $$->val = ($7) ? $7->val : 0;
 811                                   trackchanuse($5, $2, 'A'); trackrun($$);
 812                                 }
 813         | LEN l_par varref r_par        { $$ = nn($3, LEN, $3, ZN); }
 814         | ENABLED l_par expr r_par      { $$ = nn(ZN, ENABLED, $3, ZN); has_enabled++; }
 815         | GET_P l_par expr r_par        { $$ = nn(ZN, GET_P, $3, ZN); has_priority++; }
 816         | varref RCV            { Expand_Ok++; }
 817           '[' rargs ']'         { Expand_Ok--; has_io++;
 818                                   $$ = nn($1, 'R', $1, $5);
 819                                 }
 820         | varref R_RCV          { Expand_Ok++; }
 821           '[' rargs ']'         { Expand_Ok--; has_io++;
 822                                   $$ = nn($1, 'R', $1, $5);
 823                                   $$->val = has_random = 1;
 824                                 }
 825         | varref                { $$ = $1; trapwonly($1 /*, "varref" */); }
 826         | cexpr                 { $$ = $1; }
 827         | CONST                 { $$ = nn(ZN,CONST,ZN,ZN);
 828                                   $$->ismtyp = $1->ismtyp;
 829                                   $$->val = $1->val;
 830                                 }
 831         | TIMEOUT               { $$ = nn(ZN,TIMEOUT, ZN, ZN); }
 832         | NONPROGRESS           { $$ = nn(ZN,NONPROGRESS, ZN, ZN);
 833                                   has_np++;
 834                                 }
 835         | PC_VAL l_par expr r_par       { $$ = nn(ZN, PC_VAL, $3, ZN);
 836                                   has_pcvalue++;
 837                                 }
 838         | PNAME '[' expr ']' '@' NAME
 839                                 { $$ = rem_lab($1->sym, $3, $6->sym); }
 840         | PNAME '[' expr ']' ':' pfld
 841                                 { $$ = rem_var($1->sym, $3, $6->sym, $6->lft); }
 842         | PNAME '@' NAME        { $$ = rem_lab($1->sym, ZN, $3->sym); }
 843         | PNAME ':' pfld        { $$ = rem_var($1->sym, ZN, $3->sym, $3->lft); }
 844         | ltl_expr              { $$ = $1; /* sanity_check($1); */ }
 845         ;
 846
 847 Opt_priority:   /* none */      { $$ = ZN; }
 848         | PRIORITY CONST        { $$ = $2; has_priority++; }
 849         ;
 850
 851 full_expr:      expr            { $$ = $1; }
 852         | Expr          { $$ = $1; }
 853         ;
 854
 855 ltl_expr: expr UNTIL expr       { $$ = nn(ZN, UNTIL,   $1, $3); }
 856         | expr RELEASE expr     { $$ = nn(ZN, RELEASE, $1, $3); }
 857         | expr WEAK_UNTIL expr  { $$ = nn(ZN, ALWAYS, $1, ZN);
 858                                   $$ = nn(ZN, OR, $$, nn(ZN, UNTIL, $1, $3));
 859                                 }
 860         | expr IMPLIES expr     {
 861                                 $$ = nn(ZN, '!', $1, ZN);
 862                                 $$ = nn(ZN, OR,  $$, $3);
 863                                 }
 864         | expr EQUIV expr       { $$ = nn(ZN, EQUIV,   $1, $3); }
 865         | NEXT expr       %prec NEG { $$ = nn(ZN, NEXT,  $2, ZN); }
 866         | ALWAYS expr     %prec NEG { $$ = nn(ZN, ALWAYS,$2, ZN); }
 867         | EVENTUALLY expr %prec NEG { $$ = nn(ZN, EVENTUALLY, $2, ZN); }
 868         ;
 869
 870         /* an Expr cannot be negated - to protect Probe expressions */
 871 Expr    : Probe                 { $$ = $1; }
 872         | l_par Expr r_par              { $$ = $2; }
 873         | Expr AND Expr         { $$ = nn(ZN, AND, $1, $3); }
 874         | Expr AND expr         { $$ = nn(ZN, AND, $1, $3); }
 875         | expr AND Expr         { $$ = nn(ZN, AND, $1, $3); }
 876         | Expr OR  Expr         { $$ = nn(ZN,  OR, $1, $3); }
 877         | Expr OR  expr         { $$ = nn(ZN,  OR, $1, $3); }
 878         | expr OR  Expr         { $$ = nn(ZN,  OR, $1, $3); }
 879         ;
 880
 881 Probe   : FULL l_par varref r_par       { $$ = nn($3,  FULL, $3, ZN); }
 882         | NFULL l_par varref r_par      { $$ = nn($3, NFULL, $3, ZN); }
 883         | EMPTY l_par varref r_par      { $$ = nn($3, EMPTY, $3, ZN); }
 884         | NEMPTY l_par varref r_par     { $$ = nn($3,NEMPTY, $3, ZN); }
 885         ;
 886
 887 Opt_enabler:    /* none */      { $$ = ZN; }
 888         | PROVIDED l_par full_expr r_par        { if (!proper_enabler($3))
 889                                   {     non_fatal("invalid PROVIDED clause",
 890                                                 (char *)0);
 891                                         $$ = ZN;
 892                                   } else
 893                                         $$ = $3;
 894                                  }
 895         | PROVIDED error        { $$ = ZN;
 896                                   non_fatal("usage: provided ( ..expr.. )",
 897                                         (char *)0);
 898                                 }
 899         ;
 900
 901 basetype: TYPE                  { $$->sym = ZS;
 902                                   $$->val = $1->val;
 903                                   if ($$->val == UNSIGNED)
 904                                   fatal("unsigned cannot be used as mesg type", 0);
 905                                 }
 906         | UNAME                 { $$->sym = $1->sym;
 907                                   $$->val = STRUCT;
 908                                 }
 909         | error                 /* e.g., unsigned ':' const */
 910         ;
 911
 912 typ_list: basetype              { $$ = nn($1, $1->val, ZN, ZN); }
 913         | basetype ',' typ_list { $$ = nn($1, $1->val, ZN, $3); }
 914         ;
 915
 916 two_args:       expr ',' expr   { $$ = nn(ZN, ',', $1, $3); }
 917         ;
 918
 919 args    : /* empty */           { $$ = ZN; }
 920         | arg                   { $$ = $1; }
 921         ;
 922
 923 prargs  : /* empty */           { $$ = ZN; }
 924         | ',' arg               { $$ = $2; }
 925         ;
 926
 927 margs   : arg                   { $$ = $1; }
 928         | expr l_par arg r_par  { if ($1->ntyp == ',')
 929                                         $$ = tail_add($1, $3);
 930                                   else
 931                                         $$ = nn(ZN, ',', $1, $3);
 932                                 }
 933         ;
 934
 935 arg     : expr                  { if ($1->ntyp == ',')
 936                                         $$ = $1;
 937                                   else
 938                                         $$ = nn(ZN, ',', $1, ZN);
 939                                 }
 940         | expr ',' arg          { if ($1->ntyp == ',')
 941                                         $$ = tail_add($1, $3);
 942                                   else
 943                                         $$ = nn(ZN, ',', $1, $3);
 944                                 }
 945         ;
 946
 947 rarg    : varref                { $$ = $1; trackvar($1, $1);
 948                                   trapwonly($1 /*, "rarg" */); }
 949         | EVAL l_par expr r_par { $$ = nn(ZN,EVAL,$3,ZN);
 950                                   trapwonly($1 /*, "eval rarg" */); }
 951         | CONST                 { $$ = nn(ZN,CONST,ZN,ZN);
 952                                   $$->ismtyp = $1->ismtyp;
 953                                   $$->val = $1->val;
 954                                 }
 955         | '-' CONST %prec UMIN  { $$ = nn(ZN,CONST,ZN,ZN);
 956                                   $$->val = - ($2->val);
 957                                 }
 958         ;
 959
 960 rargs   : rarg                  { if ($1->ntyp == ',')
 961                                         $$ = $1;
 962                                   else
 963                                         $$ = nn(ZN, ',', $1, ZN);
 964                                 }
 965         | rarg ',' rargs        { if ($1->ntyp == ',')
 966                                         $$ = tail_add($1, $3);
 967                                   else
 968                                         $$ = nn(ZN, ',', $1, $3);
 969                                 }
 970         | rarg l_par rargs r_par        { if ($1->ntyp == ',')
 971                                         $$ = tail_add($1, $3);
 972                                   else
 973                                         $$ = nn(ZN, ',', $1, $3);
 974                                 }
 975         | l_par rargs r_par             { $$ = $2; }
 976         ;
 977
 978 nlst    : NAME                  { $$ = nn($1, NAME, ZN, ZN);
 979                                   $$ = nn(ZN, ',', $$, ZN); }
 980         | nlst NAME             { $$ = nn($2, NAME, ZN, ZN);
 981                                   $$ = nn(ZN, ',', $$, $1);
 982                                 }
 983         | nlst ','              { $$ = $1; /* commas optional */ }
 984         ;
 985 %%
 986
 987 #define binop(n, sop)   fprintf(fd, "("); recursive(fd, n->lft); \
 988                         fprintf(fd, ") %s (", sop); recursive(fd, n->rgt); \
 989                         fprintf(fd, ")");
 990 #define unop(n, sop)    fprintf(fd, "%s (", sop); recursive(fd, n->lft); \
 991                         fprintf(fd, ")");
 992
 993 static void
 994 recursive(FILE *fd, Lextok *n)
 995 {
 996         if (n)
 997         switch (n->ntyp) {
 998         case NEXT:
 999                 unop(n, "X");
1000                 break;
1001         case ALWAYS:
1002                 unop(n, "[]");
1003                 break;
1004         case EVENTUALLY:
1005                 unop(n, "<>");
1006                 break;
1007         case '!':
1008                 unop(n, "!");
1009                 break;
1010         case UNTIL:
1011                 binop(n, "U");
1012                 break;
1013         case WEAK_UNTIL:
1014                 binop(n, "W");
1015                 break;
1016         case RELEASE: /* see http://en.wikipedia.org/wiki/Linear_temporal_logic */
1017                 binop(n, "V");
1018                 break;
1019         case OR:
1020                 binop(n, "||");
1021                 break;
1022         case AND:
1023                 binop(n, "&&");
1024                 break;
1025         case IMPLIES:
1026                 binop(n, "->");
1027                 break;
1028         case EQUIV:
1029                 binop(n, "<->");
1030                 break;
1031         case C_EXPR:
1032                 fprintf(fd, "c_expr { %s }", put_inline(fd, n->sym->name));
1033                 break;
1034         default:
1035                 comment(fd, n, 0);
1036                 break;
1037         }
1038 }
1039
1040 static Lextok *
1041 ltl_to_string(Lextok *n)
1042 {       Lextok *m = nn(ZN, 0, ZN, ZN);
1043         char *retval;
1044         char ltl_formula[2048];
1045         FILE *tf = fopen(TMP_FILE1, "w+"); /* tmpfile() fails on Windows 7 */
1046
1047         /* convert the parsed ltl to a string
1048            by writing into a file, using existing functions,
1049            and then passing it to the existing interface for
1050            conversion into a never claim
1051           (this means parsing everything twice, which is
1052            a little redundant, but adds only miniscule overhead)
1053          */
1054
1055         if (!tf)
1056         {       fatal("cannot create temporary file", (char *) 0);
1057         }
1058         dont_simplify = 1;
1059         recursive(tf, n);
1060         dont_simplify = 0;
1061         (void) fseek(tf, 0L, SEEK_SET);
1062
1063         memset(ltl_formula, 0, sizeof(ltl_formula));
1064         retval = fgets(ltl_formula, sizeof(ltl_formula), tf);
1065         fclose(tf);
1066
1067         (void) unlink(TMP_FILE1);
1068
1069         if (!retval)
1070         {       printf("%p\n", retval);
1071                 fatal("could not translate ltl ltl_formula", 0);
1072         }
1073
1074         if (1) printf("ltl %s: %s\n", ltl_name, ltl_formula);
1075
1076         m->sym = lookup(ltl_formula);
1077
1078         return m;
1079 }
1080
1081 int
1082 is_temporal(int t)
1083 {
1084         return (t == EVENTUALLY || t == ALWAYS || t == UNTIL
1085              || t == WEAK_UNTIL || t == RELEASE);
1086 }
1087
1088 int
1089 is_boolean(int t)
1090 {
1091         return (t == AND || t == OR || t == IMPLIES || t == EQUIV);
1092 }
1093
1094 #if 0
1095 /* flags correct formula like: ltl { true U (true U true) } */
1096 void
1097 sanity_check(Lextok *t) /* check proper embedding of ltl_expr */
1098 {
1099         if (!t) return;
1100         sanity_check(t->lft);
1101         sanity_check(t->rgt);
1102
1103         if (t->lft && t->rgt)
1104         {       if (!is_boolean(t->ntyp)
1105                 &&  (is_temporal(t->lft->ntyp)
1106                 ||   is_temporal(t->rgt->ntyp)))
1107                 {       printf("spin: attempt to apply '");
1108                         explain(t->ntyp);
1109                         printf("' to '");
1110                         explain(t->lft->ntyp);
1111                         printf("' and '");
1112                         explain(t->rgt->ntyp);
1113                         printf("'\n");
1114         /*              non_fatal("missing parentheses?", (char *)0); */
1115         }       }
1116 }
1117 #endif
1118
1119 void
1120 yyerror(char *fmt, ...)
1121 {
1122         non_fatal(fmt, (char *) 0);
1123 }