verif/Spin/Src5.1.6/main.c

   1 /***** spin: main.c *****/
   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 #include <stdlib.h>
  13 #include "spin.h"
  14 #include "version.h"
  15 #include <signal.h>
  16 /* #include <malloc.h> */
  17 #include <time.h>
  18 #ifdef PC
  19 #include <io.h>
  20 extern int unlink(const char *);
  21 #else
  22 #include <unistd.h>
  23 #endif
  24 #include "y.tab.h"
  25
  26 extern int      DstepStart, lineno, tl_terse;
  27 extern FILE     *yyin, *yyout, *tl_out;
  28 extern Symbol   *context;
  29 extern char     *claimproc;
  30 extern void     repro_src(void);
  31 extern void     qhide(int);
  32
  33 Symbol  *Fname, *oFname;
  34
  35 int     Etimeouts;      /* nr timeouts in program */
  36 int     Ntimeouts;      /* nr timeouts in never claim */
  37 int     analyze, columns, dumptab, has_remote, has_remvar;
  38 int     interactive, jumpsteps, m_loss, nr_errs, cutoff;
  39 int     s_trail, ntrail, verbose, xspin, notabs, rvopt;
  40 int     no_print, no_wrapup, Caccess, limited_vis, like_java;
  41 int     separate;       /* separate compilation */
  42 int     export_ast;     /* pangen5.c */
  43
  44 int     merger = 1, deadvar = 1, ccache = 1;
  45
  46 static int preprocessonly, SeedUsed;
  47 static int seedy;       /* be verbose about chosen seed */
  48 static int inlineonly;  /* show inlined code */
  49 static int dataflow = 1;
  50
  51 #if 0
  52 meaning of flags on verbose:
  53         1       -g global variable values
  54         2       -l local variable values
  55         4       -p all process actions
  56         8       -r receives
  57         16      -s sends
  58         32      -v verbose
  59         64      -w very verbose
  60 #endif
  61
  62 static char     Operator[] = "operator: ";
  63 static char     Keyword[]  = "keyword: ";
  64 static char     Function[] = "function-name: ";
  65 static char     **add_ltl  = (char **)0;
  66 static char     **ltl_file = (char **)0;
  67 static char     **nvr_file = (char **)0;
  68 static char     *PreArg[64];
  69 static int      PreCnt = 0;
  70 static char     out1[64];
  71 void    explain(int);
  72
  73 #ifndef CPP
  74                 /* OS2:         "spin -Picc -E/Pd+ -E/Q+"    */
  75                 /* Visual C++:  "spin -PCL  -E/E             */
  76 #ifdef PC
  77 #define CPP     "gcc -E -x c"   /* most systems have gcc anyway */
  78                                 /* else use "cpp" */
  79 #else
  80 #ifdef SOLARIS
  81 #define CPP     "/usr/ccs/lib/cpp"
  82 #else
  83 #if defined(__FreeBSD__) || defined(__OpenBSD__) || defined(__NetBSD__)
  84 #define CPP     "cpp"
  85 #else
  86 #define CPP     "/lib/cpp"      /* classic Unix systems */
  87 #endif
  88 #endif
  89 #endif
  90
  91 #endif
  92 static char     *PreProc = CPP;
  93 extern int      depth; /* at least some steps were made */
  94
  95 void
  96 alldone(int estatus)
  97 {
  98         if (preprocessonly == 0
  99         &&  strlen(out1) > 0)
 100                 (void) unlink((const char *)out1);
 101
 102         if (seedy && !analyze && !export_ast
 103         && !s_trail && !preprocessonly && depth > 0)
 104                 printf("seed used: %d\n", SeedUsed);
 105
 106         if (xspin && (analyze || s_trail))
 107         {       if (estatus)
 108                         printf("spin: %d error(s) - aborting\n",
 109                         estatus);
 110                 else
 111                         printf("Exit-Status 0\n");
 112         }
 113         exit(estatus);
 114 }
 115
 116 void
 117 preprocess(char *a, char *b, int a_tmp)
 118 {       char precmd[1024], cmd[2048]; int i;
 119 #ifdef PC
 120         extern int try_zpp(char *, char *);
 121         if (PreCnt == 0 && try_zpp(a, b)) goto out;
 122 #endif
 123         strcpy(precmd, PreProc);
 124         for (i = 1; i <= PreCnt; i++)
 125         {       strcat(precmd, " ");
 126                 strcat(precmd, PreArg[i]);
 127         }
 128         if (strlen(precmd) > sizeof(precmd))
 129         {       fprintf(stdout, "spin: too many -D args, aborting\n");
 130                 alldone(1);
 131         }
 132         sprintf(cmd, "%s %s > %s", precmd, a, b);
 133         if (system((const char *)cmd))
 134         {       (void) unlink((const char *) b);
 135                 if (a_tmp) (void) unlink((const char *) a);
 136                 fprintf(stdout, "spin: preprocessing failed\n");        /* 4.1.2 was stderr */
 137                 alldone(1); /* no return, error exit */
 138         }
 139 #ifdef PC
 140 out:
 141 #endif
 142         if (a_tmp) (void) unlink((const char *) a);
 143 }
 144
 145 FILE *
 146 cpyfile(char *src, char *tgt)
 147 {       FILE *inp, *out;
 148         char buf[1024];
 149
 150         inp = fopen(src, "r");
 151         out = fopen(tgt, "w");
 152         if (!inp || !out)
 153         {       printf("spin: cannot cp %s to %s\n", src, tgt);
 154                 alldone(1);
 155         }
 156         while (fgets(buf, 1024, inp))
 157                 fprintf(out, "%s", buf);
 158         fclose(inp);
 159         return out;
 160 }
 161
 162 void
 163 usage(void)
 164 {
 165         printf("use: spin [-option] ... [-option] file\n");
 166         printf("\tNote: file must always be the last argument\n");
 167         printf("\t-A apply slicing algorithm\n");
 168         printf("\t-a generate a verifier in pan.c\n");
 169         printf("\t-B no final state details in simulations\n");
 170         printf("\t-b don't execute printfs in simulation\n");
 171         printf("\t-C print channel access info (combine with -g etc.)\n");
 172         printf("\t-c columnated -s -r simulation output\n");
 173         printf("\t-d produce symbol-table information\n");
 174         printf("\t-Dyyy pass -Dyyy to the preprocessor\n");
 175         printf("\t-Eyyy pass yyy to the preprocessor\n");
 176         printf("\t-f \"..formula..\"  translate LTL ");
 177         printf("into never claim\n");
 178         printf("\t-F file  like -f, but with the LTL ");
 179         printf("formula stored in a 1-line file\n");
 180         printf("\t-g print all global variables\n");
 181         printf("\t-h  at end of run, print value of seed for random nr generator used\n");
 182         printf("\t-i interactive (random simulation)\n");
 183         printf("\t-I show result of inlining and preprocessing\n");
 184         printf("\t-J reverse eval order of nested unlesses\n");
 185         printf("\t-jN skip the first N steps ");
 186         printf("in simulation trail\n");
 187         printf("\t-l print all local variables\n");
 188         printf("\t-M print msc-flow in Postscript\n");
 189         printf("\t-m lose msgs sent to full queues\n");
 190         printf("\t-N file use never claim stored in file\n");
 191         printf("\t-nN seed for random nr generator\n");
 192         printf("\t-o1 turn off dataflow-optimizations in verifier\n");
 193         printf("\t-o2 don't hide write-only variables in verifier\n");
 194         printf("\t-o3 turn off statement merging in verifier\n");
 195         printf("\t-Pxxx use xxx for preprocessing\n");
 196         printf("\t-p print all statements\n");
 197         printf("\t-qN suppress io for queue N in printouts\n");
 198         printf("\t-r print receive events\n");
 199         printf("\t-S1 and -S2 separate pan source for claim and model\n");
 200         printf("\t-s print send events\n");
 201         printf("\t-T do not indent printf output\n");
 202         printf("\t-t[N] follow [Nth] simulation trail\n");
 203         printf("\t-Uyyy pass -Uyyy to the preprocessor\n");
 204         printf("\t-uN stop a simulation run after N steps\n");
 205         printf("\t-v verbose, more warnings\n");
 206         printf("\t-w very verbose (when combined with -l or -g)\n");
 207         printf("\t-[XYZ] reserved for use by xspin interface\n");
 208         printf("\t-V print version number and exit\n");
 209         alldone(1);
 210 }
 211
 212 void
 213 optimizations(int nr)
 214 {
 215         switch (nr) {
 216         case '1':
 217                 dataflow = 1 - dataflow; /* dataflow */
 218                 if (verbose&32)
 219                 printf("spin: dataflow optimizations turned %s\n",
 220                         dataflow?"on":"off");
 221                 break;
 222         case '2':
 223                 /* dead variable elimination */
 224                 deadvar = 1 - deadvar;
 225                 if (verbose&32)
 226                 printf("spin: dead variable elimination turned %s\n",
 227                         deadvar?"on":"off");
 228                 break;
 229         case '3':
 230                 /* statement merging */
 231                 merger = 1 - merger;
 232                 if (verbose&32)
 233                 printf("spin: statement merging turned %s\n",
 234                         merger?"on":"off");
 235                 break;
 236
 237         case '4':
 238                 /* rv optimization */
 239                 rvopt = 1 - rvopt;
 240                 if (verbose&32)
 241                 printf("spin: rendezvous optimization turned %s\n",
 242                         rvopt?"on":"off");
 243                 break;
 244         case '5':
 245                 /* case caching */
 246                 ccache = 1 - ccache;
 247                 if (verbose&32)
 248                 printf("spin: case caching turned %s\n",
 249                         ccache?"on":"off");
 250                 break;
 251         default:
 252                 printf("spin: bad or missing parameter on -o\n");
 253                 usage();
 254                 break;
 255         }
 256 }
 257
 258 #if 0
 259 static int
 260 Rename(const char *old, char *new)
 261 {       FILE *fo, *fn;
 262         char buf[1024];
 263
 264         if ((fo = fopen(old, "r")) == NULL)
 265         {       printf("spin: cannot open %s\n", old);
 266                 return 1;
 267         }
 268         if ((fn = fopen(new, "w")) == NULL)
 269         {       printf("spin: cannot create %s\n", new);
 270                 fclose(fo);
 271                 return 2;
 272         }
 273         while (fgets(buf, 1024, fo))
 274                 fputs(buf, fn);
 275
 276         fclose(fo);
 277         fclose(fn);
 278
 279         return 0;       /* success */
 280 }
 281 #endif
 282
 283 int
 284 main(int argc, char *argv[])
 285 {       Symbol *s;
 286         int T = (int) time((time_t *)0);
 287         int usedopts = 0;
 288         extern void ana_src(int, int);
 289
 290         yyin  = stdin;
 291         yyout = stdout;
 292         tl_out = stdout;
 293
 294         /* unused flags: e, w, x, y, z, A, G, I, L, O, Q, R, S, T, W */
 295         while (argc > 1 && argv[1][0] == '-')
 296         {       switch (argv[1][1]) {
 297
 298                 /* generate code for separate compilation: S1 or S2 */
 299                 case 'S': separate = atoi(&argv[1][2]);
 300                           /* fall through */
 301                 case 'a': analyze  = 1; break;
 302
 303                 case 'A': export_ast = 1; break;
 304                 case 'B': no_wrapup = 1; break;
 305                 case 'b': no_print = 1; break;
 306                 case 'C': Caccess = 1; break;
 307                 case 'c': columns = 1; break;
 308                 case 'D': PreArg[++PreCnt] = (char *) &argv[1][0];
 309                           break;        /* define */
 310                 case 'd': dumptab =  1; break;
 311                 case 'E': PreArg[++PreCnt] = (char *) &argv[1][2];
 312                           break;
 313                 case 'F': ltl_file = (char **) (argv+2);
 314                           argc--; argv++; break;
 315                 case 'f': add_ltl = (char **) argv;
 316                           argc--; argv++; break;
 317                 case 'g': verbose +=  1; break;
 318                 case 'h': seedy = 1; break;
 319                 case 'i': interactive = 1; break;
 320                 case 'I': inlineonly = 1; break;
 321                 case 'J': like_java = 1; break;
 322                 case 'j': jumpsteps = atoi(&argv[1][2]); break;
 323                 case 'l': verbose +=  2; break;
 324                 case 'M': columns = 2; break;
 325                 case 'm': m_loss   =  1; break;
 326                 case 'N': nvr_file = (char **) (argv+2);
 327                           argc--; argv++; break;
 328                 case 'n': T = atoi(&argv[1][2]); tl_terse = 1; break;
 329                 case 'o': optimizations(argv[1][2]);
 330                           usedopts = 1; break;
 331                 case 'P': PreProc = (char *) &argv[1][2]; break;
 332                 case 'p': verbose +=  4; break;
 333                 case 'q': if (isdigit(argv[1][2]))
 334                                 qhide(atoi(&argv[1][2]));
 335                           break;
 336                 case 'r': verbose +=  8; break;
 337                 case 's': verbose += 16; break;
 338                 case 'T': notabs = 1; break;
 339                 case 't': s_trail  =  1;
 340                           if (isdigit(argv[1][2]))
 341                                 ntrail = atoi(&argv[1][2]);
 342                           break;
 343                 case 'U': PreArg[++PreCnt] = (char *) &argv[1][0];
 344                           break;        /* undefine */
 345                 case 'u': cutoff = atoi(&argv[1][2]); break;    /* new 3.4.14 */
 346                 case 'v': verbose += 32; break;
 347                 case 'V': printf("%s\n", SpinVersion);
 348                           alldone(0);
 349                           break;
 350                 case 'w': verbose += 64; break;
 351                 case 'X': xspin = notabs = 1;
 352 #ifndef PC
 353                           signal(SIGPIPE, alldone); /* not posix... */
 354 #endif
 355                           break;
 356                 case 'Y': limited_vis = 1; break;       /* used by xspin */
 357                 case 'Z': preprocessonly = 1; break;    /* used by xspin */
 358
 359                 default : usage(); break;
 360                 }
 361                 argc--; argv++;
 362         }
 363         if (usedopts && !analyze)
 364                 printf("spin: warning -o[123] option ignored in simulations\n");
 365
 366         if (ltl_file)
 367         {       char formula[4096];
 368                 add_ltl = ltl_file-2; add_ltl[1][1] = 'f';
 369                 if (!(tl_out = fopen(*ltl_file, "r")))
 370                 {       printf("spin: cannot open %s\n", *ltl_file);
 371                         alldone(1);
 372                 }
 373                 fgets(formula, 4096, tl_out);
 374                 fclose(tl_out);
 375                 tl_out = stdout;
 376                 *ltl_file = (char *) formula;
 377         }
 378         if (argc > 1)
 379         {       char cmd[128], out2[64];
 380
 381                 /* must remain in current dir */
 382                 strcpy(out1, "pan.pre");
 383
 384                 if (add_ltl || nvr_file)
 385                         strcpy(out2, "pan.___");
 386
 387                 if (add_ltl)
 388                 {       tl_out = cpyfile(argv[1], out2);
 389                         nr_errs = tl_main(2, add_ltl);  /* in tl_main.c */
 390                         fclose(tl_out);
 391                         preprocess(out2, out1, 1);
 392                 } else if (nvr_file)
 393                 {       FILE *fd; char buf[1024];
 394
 395                         if ((fd = fopen(*nvr_file, "r")) == NULL)
 396                         {       printf("spin: cannot open %s\n",
 397                                         *nvr_file);
 398                                 alldone(1);
 399                         }
 400                         tl_out = cpyfile(argv[1], out2);
 401                         while (fgets(buf, 1024, fd))
 402                                 fprintf(tl_out, "%s", buf);
 403                         fclose(tl_out);
 404                         fclose(fd);
 405                         preprocess(out2, out1, 1);
 406                 } else
 407                         preprocess(argv[1], out1, 0);
 408
 409                 if (preprocessonly)
 410                         alldone(0);
 411
 412                 if (!(yyin = fopen(out1, "r")))
 413                 {       printf("spin: cannot open %s\n", out1);
 414                         alldone(1);
 415                 }
 416
 417                 if (strncmp(argv[1], "progress", (size_t) 8) == 0
 418                 ||  strncmp(argv[1], "accept", (size_t) 6) == 0)
 419                         sprintf(cmd, "_%s", argv[1]);
 420                 else
 421                         strcpy(cmd, argv[1]);
 422                 oFname = Fname = lookup(cmd);
 423                 if (oFname->name[0] == '\"')
 424                 {       int i = (int) strlen(oFname->name);
 425                         oFname->name[i-1] = '\0';
 426                         oFname = lookup(&oFname->name[1]);
 427                 }
 428         } else
 429         {       oFname = Fname = lookup("<stdin>");
 430                 if (add_ltl)
 431                 {       if (argc > 0)
 432                                 exit(tl_main(2, add_ltl));
 433                         printf("spin: missing argument to -f\n");
 434                         alldone(1);
 435                 }
 436                 printf("%s\n", SpinVersion);
 437                 printf("reading input from stdin:\n");
 438                 fflush(stdout);
 439         }
 440         if (columns == 2)
 441         {       extern void putprelude(void);
 442                 if (xspin || verbose&(1|4|8|16|32))
 443                 {       printf("spin: -c precludes all flags except -t\n");
 444                         alldone(1);
 445                 }
 446                 putprelude();
 447         }
 448         if (columns && !(verbose&8) && !(verbose&16))
 449                 verbose += (8+16);
 450         if (columns == 2 && limited_vis)
 451                 verbose += (1+4);
 452         Srand((unsigned int) T);        /* defined in run.c */
 453         SeedUsed = T;
 454         s = lookup("_");        s->type = PREDEF; /* write-only global var */
 455         s = lookup("_p");       s->type = PREDEF;
 456         s = lookup("_pid");     s->type = PREDEF;
 457         s = lookup("_last");    s->type = PREDEF;
 458         s = lookup("_nr_pr");   s->type = PREDEF; /* new 3.3.10 */
 459
 460         yyparse();
 461         fclose(yyin);
 462         loose_ends();
 463
 464         if (inlineonly)
 465         {       repro_src();
 466                 return 0;
 467         }
 468
 469         chanaccess();
 470         if (!Caccess)
 471         {       if (!s_trail && (dataflow || merger))
 472                         ana_src(dataflow, merger);
 473                 sched();
 474                 alldone(nr_errs);
 475         }
 476         return 0;
 477 }
 478
 479 int
 480 yywrap(void)    /* dummy routine */
 481 {
 482         return 1;
 483 }
 484
 485 void
 486 non_fatal(char *s1, char *s2)
 487 {       extern int yychar; extern char yytext[];
 488
 489         printf("spin: line %3d %s, Error: ",
 490                 lineno, Fname?Fname->name:"nofilename");
 491         if (s2)
 492                 printf(s1, s2);
 493         else
 494                 printf(s1);
 495         if (yychar != -1 && yychar != 0)
 496         {       printf("        saw '");
 497                 explain(yychar);
 498                 printf("'");
 499         }
 500         if (strlen(yytext)>1)
 501                 printf(" near '%s'", yytext);
 502         printf("\n");
 503         nr_errs++;
 504 }
 505
 506 void
 507 fatal(char *s1, char *s2)
 508 {
 509         non_fatal(s1, s2);
 510         alldone(1);
 511 }
 512
 513 char *
 514 emalloc(size_t n)
 515 {       char *tmp;
 516
 517         if (n == 0)
 518                 return NULL;    /* robert shelton 10/20/06 */
 519
 520         if (!(tmp = (char *) malloc(n)))
 521                 fatal("not enough memory", (char *)0);
 522         memset(tmp, 0, n);
 523         return tmp;
 524 }
 525
 526 void
 527 trapwonly(Lextok *n /* , char *unused */)
 528 {       extern int realread;
 529         short i = (n->sym)?n->sym->type:0;
 530
 531         if (i != MTYPE
 532         &&  i != BIT
 533         &&  i != BYTE
 534         &&  i != SHORT
 535         &&  i != INT
 536         &&  i != UNSIGNED)
 537                 return;
 538
 539         if (realread)
 540         n->sym->hidden |= 128;  /* var is read at least once */
 541 }
 542
 543 void
 544 setaccess(Symbol *sp, Symbol *what, int cnt, int t)
 545 {       Access *a;
 546
 547         for (a = sp->access; a; a = a->lnk)
 548                 if (a->who == context
 549                 &&  a->what == what
 550                 &&  a->cnt == cnt
 551                 &&  a->typ == t)
 552                         return;
 553
 554         a = (Access *) emalloc(sizeof(Access));
 555         a->who = context;
 556         a->what = what;
 557         a->cnt = cnt;
 558         a->typ = t;
 559         a->lnk = sp->access;
 560         sp->access = a;
 561 }
 562
 563 Lextok *
 564 nn(Lextok *s, int t, Lextok *ll, Lextok *rl)
 565 {       Lextok *n = (Lextok *) emalloc(sizeof(Lextok));
 566         static int warn_nn = 0;
 567
 568         n->ntyp = (short) t;
 569         if (s && s->fn)
 570         {       n->ln = s->ln;
 571                 n->fn = s->fn;
 572         } else if (rl && rl->fn)
 573         {       n->ln = rl->ln;
 574                 n->fn = rl->fn;
 575         } else if (ll && ll->fn)
 576         {       n->ln = ll->ln;
 577                 n->fn = ll->fn;
 578         } else
 579         {       n->ln = lineno;
 580                 n->fn = Fname;
 581         }
 582         if (s) n->sym  = s->sym;
 583         n->lft  = ll;
 584         n->rgt  = rl;
 585         n->indstep = DstepStart;
 586
 587         if (t == TIMEOUT) Etimeouts++;
 588
 589         if (!context) return n;
 590
 591         if (t == 'r' || t == 's')
 592                 setaccess(n->sym, ZS, 0, t);
 593         if (t == 'R')
 594                 setaccess(n->sym, ZS, 0, 'P');
 595
 596         if (context->name == claimproc)
 597         {       int forbidden = separate;
 598                 switch (t) {
 599                 case ASGN:
 600                         printf("spin: Warning, never claim has side-effect\n");
 601                         break;
 602                 case 'r': case 's':
 603                         non_fatal("never claim contains i/o stmnts",(char *)0);
 604                         break;
 605                 case TIMEOUT:
 606                         /* never claim polls timeout */
 607                         if (Ntimeouts && Etimeouts)
 608                                 forbidden = 0;
 609                         Ntimeouts++; Etimeouts--;
 610                         break;
 611                 case LEN: case EMPTY: case FULL:
 612                 case 'R': case NFULL: case NEMPTY:
 613                         /* status becomes non-exclusive */
 614                         if (n->sym && !(n->sym->xu&XX))
 615                         {       n->sym->xu |= XX;
 616                                 if (separate == 2) {
 617                                 printf("spin: warning, make sure that the S1 model\n");
 618                                 printf("      also polls channel '%s' in its claim\n",
 619                                 n->sym->name);
 620                         }       }
 621                         forbidden = 0;
 622                         break;
 623                 case 'c':
 624                         AST_track(n, 0);        /* register as a slice criterion */
 625                         /* fall thru */
 626                 default:
 627                         forbidden = 0;
 628                         break;
 629                 }
 630                 if (forbidden)
 631                 {       printf("spin: never, saw "); explain(t); printf("\n");
 632                         fatal("incompatible with separate compilation",(char *)0);
 633                 }
 634         } else if ((t == ENABLED || t == PC_VAL) && !(warn_nn&t))
 635         {       printf("spin: Warning, using %s outside never claim\n",
 636                         (t == ENABLED)?"enabled()":"pc_value()");
 637                 warn_nn |= t;
 638         } else if (t == NONPROGRESS)
 639         {       fatal("spin: Error, using np_ outside never claim\n", (char *)0);
 640         }
 641         return n;
 642 }
 643
 644 Lextok *
 645 rem_lab(Symbol *a, Lextok *b, Symbol *c)        /* proctype name, pid, label name */
 646 {       Lextok *tmp1, *tmp2, *tmp3;
 647
 648         has_remote++;
 649         c->type = LABEL;        /* refered to in global context here */
 650         fix_dest(c, a);         /* in case target of rem_lab is jump */
 651         tmp1 = nn(ZN, '?',   b, ZN); tmp1->sym = a;
 652         tmp1 = nn(ZN, 'p', tmp1, ZN);
 653         tmp1->sym = lookup("_p");
 654         tmp2 = nn(ZN, NAME,  ZN, ZN); tmp2->sym = a;
 655         tmp3 = nn(ZN, 'q', tmp2, ZN); tmp3->sym = c;
 656         return nn(ZN, EQ, tmp1, tmp3);
 657 #if 0
 658               .---------------EQ-------.
 659              /                          \
 660            'p' -sym-> _p               'q' -sym-> c (label name)
 661            /                           /
 662          '?' -sym-> a (proctype)     NAME -sym-> a (proctype name)
 663          /
 664         b (pid expr)
 665 #endif
 666 }
 667
 668 Lextok *
 669 rem_var(Symbol *a, Lextok *b, Symbol *c, Lextok *ndx)
 670 {       Lextok *tmp1;
 671
 672         has_remote++;
 673         has_remvar++;
 674         dataflow = 0;   /* turn off dead variable resets 4.2.5 */
 675         tmp1 = nn(ZN, '?', b, ZN); tmp1->sym = a;
 676         tmp1 = nn(ZN, 'p', tmp1, ndx);
 677         tmp1->sym = c;
 678         return tmp1;
 679 #if 0
 680         cannot refer to struct elements
 681         only to scalars and arrays
 682
 683             'p' -sym-> c (variable name)
 684             / \______  possible arrayindex on c
 685            /
 686          '?' -sym-> a (proctype)
 687          /
 688         b (pid expr)
 689 #endif
 690 }
 691
 692 void
 693 explain(int n)
 694 {       FILE *fd = stdout;
 695         switch (n) {
 696         default:        if (n > 0 && n < 256)
 697                                 fprintf(fd, "'%c' = '", n);
 698                         fprintf(fd, "%d'", n);
 699                         break;
 700         case '\b':      fprintf(fd, "\\b"); break;
 701         case '\t':      fprintf(fd, "\\t"); break;
 702         case '\f':      fprintf(fd, "\\f"); break;
 703         case '\n':      fprintf(fd, "\\n"); break;
 704         case '\r':      fprintf(fd, "\\r"); break;
 705         case 'c':       fprintf(fd, "condition"); break;
 706         case 's':       fprintf(fd, "send"); break;
 707         case 'r':       fprintf(fd, "recv"); break;
 708         case 'R':       fprintf(fd, "recv poll %s", Operator); break;
 709         case '@':       fprintf(fd, "@"); break;
 710         case '?':       fprintf(fd, "(x->y:z)"); break;
 711         case ACTIVE:    fprintf(fd, "%sactive", Keyword); break;
 712         case AND:       fprintf(fd, "%s&&",     Operator); break;
 713         case ASGN:      fprintf(fd, "%s=",      Operator); break;
 714         case ASSERT:    fprintf(fd, "%sassert", Function); break;
 715         case ATOMIC:    fprintf(fd, "%satomic", Keyword); break;
 716         case BREAK:     fprintf(fd, "%sbreak",  Keyword); break;
 717         case C_CODE:    fprintf(fd, "%sc_code", Keyword); break;
 718         case C_DECL:    fprintf(fd, "%sc_decl", Keyword); break;
 719         case C_EXPR:    fprintf(fd, "%sc_expr", Keyword); break;
 720         case C_STATE:   fprintf(fd, "%sc_state",Keyword); break;
 721         case C_TRACK:   fprintf(fd, "%sc_track",Keyword); break;
 722         case CLAIM:     fprintf(fd, "%snever",  Keyword); break;
 723         case CONST:     fprintf(fd, "a constant"); break;
 724         case DECR:      fprintf(fd, "%s--",     Operator); break;
 725         case D_STEP:    fprintf(fd, "%sd_step", Keyword); break;
 726         case D_PROCTYPE: fprintf(fd, "%sd_proctype", Keyword); break;
 727         case DO:        fprintf(fd, "%sdo",     Keyword); break;
 728         case DOT:       fprintf(fd, "."); break;
 729         case ELSE:      fprintf(fd, "%selse",   Keyword); break;
 730         case EMPTY:     fprintf(fd, "%sempty",  Function); break;
 731         case ENABLED:   fprintf(fd, "%senabled",Function); break;
 732         case EQ:        fprintf(fd, "%s==",     Operator); break;
 733         case EVAL:      fprintf(fd, "%seval",   Function); break;
 734         case FI:        fprintf(fd, "%sfi",     Keyword); break;
 735         case FULL:      fprintf(fd, "%sfull",   Function); break;
 736         case GE:        fprintf(fd, "%s>=",     Operator); break;
 737         case GOTO:      fprintf(fd, "%sgoto",   Keyword); break;
 738         case GT:        fprintf(fd, "%s>",      Operator); break;
 739         case HIDDEN:    fprintf(fd, "%shidden", Keyword); break;
 740         case IF:        fprintf(fd, "%sif",     Keyword); break;
 741         case INCR:      fprintf(fd, "%s++",     Operator); break;
 742         case INAME:     fprintf(fd, "inline name"); break;
 743         case INLINE:    fprintf(fd, "%sinline", Keyword); break;
 744         case INIT:      fprintf(fd, "%sinit",   Keyword); break;
 745         case ISLOCAL:   fprintf(fd, "%slocal",  Keyword); break;
 746         case LABEL:     fprintf(fd, "a label-name"); break;
 747         case LE:        fprintf(fd, "%s<=",     Operator); break;
 748         case LEN:       fprintf(fd, "%slen",    Function); break;
 749         case LSHIFT:    fprintf(fd, "%s<<",     Operator); break;
 750         case LT:        fprintf(fd, "%s<",      Operator); break;
 751         case MTYPE:     fprintf(fd, "%smtype",  Keyword); break;
 752         case NAME:      fprintf(fd, "an identifier"); break;
 753         case NE:        fprintf(fd, "%s!=",     Operator); break;
 754         case NEG:       fprintf(fd, "%s! (not)",Operator); break;
 755         case NEMPTY:    fprintf(fd, "%snempty", Function); break;
 756         case NFULL:     fprintf(fd, "%snfull",  Function); break;
 757         case NON_ATOMIC: fprintf(fd, "sub-sequence"); break;
 758         case NONPROGRESS: fprintf(fd, "%snp_",  Function); break;
 759         case OD:        fprintf(fd, "%sod",     Keyword); break;
 760         case OF:        fprintf(fd, "%sof",     Keyword); break;
 761         case OR:        fprintf(fd, "%s||",     Operator); break;
 762         case O_SND:     fprintf(fd, "%s!!",     Operator); break;
 763         case PC_VAL:    fprintf(fd, "%spc_value",Function); break;
 764         case PNAME:     fprintf(fd, "process name"); break;
 765         case PRINT:     fprintf(fd, "%sprintf", Function); break;
 766         case PRINTM:    fprintf(fd, "%sprintm", Function); break;
 767         case PRIORITY:  fprintf(fd, "%spriority", Keyword); break;
 768         case PROCTYPE:  fprintf(fd, "%sproctype",Keyword); break;
 769         case PROVIDED:  fprintf(fd, "%sprovided",Keyword); break;
 770         case RCV:       fprintf(fd, "%s?",      Operator); break;
 771         case R_RCV:     fprintf(fd, "%s??",     Operator); break;
 772         case RSHIFT:    fprintf(fd, "%s>>",     Operator); break;
 773         case RUN:       fprintf(fd, "%srun",    Operator); break;
 774         case SEP:       fprintf(fd, "token: ::"); break;
 775         case SEMI:      fprintf(fd, ";"); break;
 776         case SHOW:      fprintf(fd, "%sshow", Keyword); break;
 777         case SND:       fprintf(fd, "%s!",      Operator); break;
 778         case STRING:    fprintf(fd, "a string"); break;
 779         case TRACE:     fprintf(fd, "%strace", Keyword); break;
 780         case TIMEOUT:   fprintf(fd, "%stimeout",Keyword); break;
 781         case TYPE:      fprintf(fd, "data typename"); break;
 782         case TYPEDEF:   fprintf(fd, "%stypedef",Keyword); break;
 783         case XU:        fprintf(fd, "%sx[rs]",  Keyword); break;
 784         case UMIN:      fprintf(fd, "%s- (unary minus)", Operator); break;
 785         case UNAME:     fprintf(fd, "a typename"); break;
 786         case UNLESS:    fprintf(fd, "%sunless", Keyword); break;
 787         }
 788 }