sys/src/cmd/spin/spinlex.c

   1 /***** spin: spinlex.c *****/
   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 #include <stdlib.h>
  10 #include <assert.h>
  11 #include <errno.h>
  12 #include <ctype.h>
  13 #include "spin.h"
  14 #include "y.tab.h"
  15
  16 #define MAXINL  16      /* max recursion depth inline fcts */
  17 #define MAXPAR  32      /* max params to an inline call */
  18 #define MAXLEN  512     /* max len of an actual parameter text */
  19
  20 typedef struct IType {
  21         Symbol *nm;             /* name of the type */
  22         Lextok *cn;             /* contents */
  23         Lextok *params;         /* formal pars if any */
  24         Lextok *rval;           /* variable to assign return value, if any */
  25         char   **anms;          /* literal text for actual pars */
  26         char   *prec;           /* precondition for c_code or c_expr */
  27         int    uiid;            /* unique inline id */
  28         int    is_expr;         /* c_expr in an ltl formula */
  29         int    dln, cln;        /* def and call linenr */
  30         Symbol *dfn, *cfn;      /* def and call filename */
  31         struct IType *nxt;      /* linked list */
  32 } IType;
  33
  34 typedef struct C_Added {
  35         Symbol *s;
  36         Symbol *t;
  37         Symbol *ival;
  38         Symbol *fnm;
  39         int     lno;
  40         struct C_Added *nxt;
  41 } C_Added;
  42
  43 extern RunList  *X;
  44 extern ProcList *rdy;
  45 extern Symbol   *Fname, *oFname;
  46 extern Symbol   *context, *owner;
  47 extern YYSTYPE  yylval;
  48 extern short    has_last, has_code, has_priority;
  49 extern int      verbose, IArgs, hastrack, separate, in_for;
  50 extern int      implied_semis, ltl_mode, in_seq, par_cnt;
  51
  52 short   has_stack = 0;
  53 int     lineno  = 1;
  54 int     scope_seq[128], scope_level = 0;
  55 char    CurScope[MAXSCOPESZ];
  56 char    yytext[2048];
  57 FILE    *yyin, *yyout;
  58
  59 static C_Added  *c_added, *c_tracked;
  60 static IType    *Inline_stub[MAXINL];
  61 static char     *ReDiRect;
  62 static char     *Inliner[MAXINL], IArg_cont[MAXPAR][MAXLEN];
  63 static unsigned char    in_comment=0;
  64 static int      IArgno = 0, Inlining = -1;
  65 static int      check_name(char *);
  66 static int      last_token = 0;
  67
  68 #define ValToken(x, y)  { if (in_comment) goto again; \
  69                         yylval = nn(ZN,0,ZN,ZN); \
  70                         yylval->val = x; \
  71                         last_token = y; \
  72                         return y; \
  73                         }
  74
  75 #define SymToken(x, y)  { if (in_comment) goto again; \
  76                         yylval = nn(ZN,0,ZN,ZN); \
  77                         yylval->sym = x; \
  78                         last_token = y; \
  79                         return y; \
  80                         }
  81
  82 static int  getinline(void);
  83 static void uninline(void);
  84
  85 static int PushBack;
  86 static int PushedBack;
  87 static char pushedback[4096];
  88
  89 static void
  90 push_back(char *s)
  91 {
  92         if (PushedBack + strlen(s) > 4094)
  93         {       fatal("select statement too large", 0);
  94         }
  95         strcat(pushedback, s);
  96         PushedBack += strlen(s);
  97 }
  98
  99 static int
 100 Getchar(void)
 101 {       int c;
 102
 103         if (PushedBack > 0 && PushBack < PushedBack)
 104         {       c = pushedback[PushBack++];
 105                 if (PushBack == PushedBack)
 106                 {       pushedback[0] = '\0';
 107                         PushBack = PushedBack = 0;
 108                 }
 109                 return c;       /* expanded select statement */
 110         }
 111         if (Inlining<0)
 112         {       c = getc(yyin);
 113         } else
 114         {       c = getinline();
 115         }
 116 #if 0
 117         if (0)
 118         {       printf("<%c:%d>[%d] ", c, c, Inlining);
 119         } else
 120         {       printf("%c", c);
 121         }
 122 #endif
 123         return c;
 124 }
 125
 126 static void
 127 Ungetch(int c)
 128 {
 129         if (PushedBack > 0 && PushBack > 0)
 130         {       PushBack--;
 131                 return;
 132         }
 133
 134         if (Inlining<0)
 135         {       ungetc(c,yyin);
 136         } else
 137         {       uninline();
 138         }
 139         if (0)
 140         {       printf("\n<bs{%d}bs>\n", c);
 141         }
 142 }
 143
 144 static int
 145 notdollar(int c)
 146 {       return (c != '$' && c != '\n');
 147 }
 148
 149 static int
 150 notquote(int c)
 151 {       return (c != '\"' && c != '\n');
 152 }
 153
 154 int
 155 isalnum_(int c)
 156 {       return (isalnum(c) || c == '_');
 157 }
 158
 159 static int
 160 isalpha_(int c)
 161 {       return isalpha(c);      /* could be macro */
 162 }
 163
 164 static int
 165 isdigit_(int c)
 166 {       return isdigit(c);      /* could be macro */
 167 }
 168
 169 static void
 170 getword(int first, int (*tst)(int))
 171 {       int i=0, c;
 172
 173         yytext[i++]= (char) first;
 174         while (tst(c = Getchar()))
 175         {       yytext[i++] = (char) c;
 176                 if (c == '\\')
 177                 {       c = Getchar();
 178                         yytext[i++] = (char) c; /* no tst */
 179         }       }
 180         yytext[i] = '\0';
 181
 182         Ungetch(c);
 183 }
 184
 185 static int
 186 follow(int tok, int ifyes, int ifno)
 187 {       int c;
 188
 189         if ((c = Getchar()) == tok)
 190         {       return ifyes;
 191         }
 192         Ungetch(c);
 193
 194         return ifno;
 195 }
 196
 197 static IType *seqnames;
 198
 199 static void
 200 def_inline(Symbol *s, int ln, char *ptr, char *prc, Lextok *nms)
 201 {       IType *tmp;
 202         int  cnt = 0;
 203         char *nw = (char *) emalloc(strlen(ptr)+1);
 204         strcpy(nw, ptr);
 205
 206         for (tmp = seqnames; tmp; cnt++, tmp = tmp->nxt)
 207                 if (!strcmp(s->name, tmp->nm->name))
 208                 {       non_fatal("procedure name %s redefined",
 209                                 tmp->nm->name);
 210                         tmp->cn = (Lextok *) nw;
 211                         tmp->params = nms;
 212                         tmp->dln = ln;
 213                         tmp->dfn = Fname;
 214                         return;
 215                 }
 216         tmp = (IType *) emalloc(sizeof(IType));
 217         tmp->nm = s;
 218         tmp->cn = (Lextok *) nw;
 219         tmp->params = nms;
 220         if (strlen(prc) > 0)
 221         {       tmp->prec = (char *) emalloc(strlen(prc)+1);
 222                 strcpy(tmp->prec, prc);
 223         }
 224         tmp->dln = ln;
 225         tmp->dfn = Fname;
 226         tmp->uiid = cnt+1;      /* so that 0 means: not an inline */
 227         tmp->nxt = seqnames;
 228         seqnames = tmp;
 229 }
 230
 231 void
 232 gencodetable(FILE *fd)
 233 {       IType *tmp;
 234         char *q;
 235         int cnt;
 236
 237         if (separate == 2) return;
 238
 239         fprintf(fd, "struct {\n");
 240         fprintf(fd, "   char *c; char *t;\n");
 241         fprintf(fd, "} code_lookup[] = {\n");
 242
 243         if (has_code)
 244         for (tmp = seqnames; tmp; tmp = tmp->nxt)
 245                 if (tmp->nm->type == CODE_FRAG
 246                 ||  tmp->nm->type == CODE_DECL)
 247                 {       fprintf(fd, "\t{ \"%s\", ",
 248                                 tmp->nm->name);
 249                         q = (char *) tmp->cn;
 250
 251                         while (*q == '\n' || *q == '\r' || *q == '\\')
 252                                 q++;
 253
 254                         fprintf(fd, "\"");
 255                         cnt = 0;
 256                         while (*q && cnt < 1024) /* pangen1.h allows 2048 */
 257                         {       switch (*q) {
 258                                 case '"':
 259                                         fprintf(fd, "\\\"");
 260                                         break;
 261                                 case '%':
 262                                         fprintf(fd, "%%");
 263                                         break;
 264                                 case '\n':
 265                                         fprintf(fd, "\\n");
 266                                         break;
 267                                 default:
 268                                         putc(*q, fd);
 269                                         break;
 270                                 }
 271                                 q++; cnt++;
 272                         }
 273                         if (*q) fprintf(fd, "...");
 274                         fprintf(fd, "\"");
 275                         fprintf(fd, " },\n");
 276                 }
 277
 278         fprintf(fd, "   { (char *) 0, \"\" }\n");
 279         fprintf(fd, "};\n");
 280 }
 281
 282 static int
 283 iseqname(char *t)
 284 {       IType *tmp;
 285
 286         for (tmp = seqnames; tmp; tmp = tmp->nxt)
 287         {       if (!strcmp(t, tmp->nm->name))
 288                         return 1;
 289         }
 290         return 0;
 291 }
 292
 293 Lextok *
 294 return_statement(Lextok *n)
 295 {
 296         if (Inline_stub[Inlining]->rval)
 297         {       Lextok *g = nn(ZN, NAME, ZN, ZN);
 298                 Lextok *h = Inline_stub[Inlining]->rval;
 299                 g->sym = lookup("rv_");
 300                 return nn(h, ASGN, h, n);
 301         } else
 302         {       fatal("return statement outside inline", (char *) 0);
 303         }
 304         return ZN;
 305 }
 306
 307 static int
 308 getinline(void)
 309 {       int c;
 310
 311         if (ReDiRect)
 312         {       c = *ReDiRect++;
 313                 if (c == '\0')
 314                 {       ReDiRect = (char *) 0;
 315                         c = *Inliner[Inlining]++;
 316                 }
 317         } else
 318         {
 319                 c = *Inliner[Inlining]++;
 320         }
 321
 322         if (c == '\0')
 323         {
 324                 lineno = Inline_stub[Inlining]->cln;
 325                 Fname  = Inline_stub[Inlining]->cfn;
 326                 Inlining--;
 327
 328 #if 0
 329                 if (verbose&32)
 330                 printf("spin: %s:%d, done inlining %s\n",
 331                         Fname, lineno, Inline_stub[Inlining+1]->nm->name);
 332 #endif
 333                 return Getchar();
 334         }
 335         return c;
 336 }
 337
 338 static void
 339 uninline(void)
 340 {
 341         if (ReDiRect)
 342                 ReDiRect--;
 343         else
 344                 Inliner[Inlining]--;
 345 }
 346
 347 int
 348 is_inline(void)
 349 {
 350         if (Inlining < 0)
 351                 return 0;       /* i.e., not an inline */
 352         if (Inline_stub[Inlining] == NULL)
 353                 fatal("unexpected, inline_stub not set", 0);
 354         return Inline_stub[Inlining]->uiid;
 355 }
 356
 357 IType *
 358 find_inline(char *s)
 359 {       IType *tmp;
 360
 361         for (tmp = seqnames; tmp; tmp = tmp->nxt)
 362                 if (!strcmp(s, tmp->nm->name))
 363                         break;
 364         if (!tmp)
 365                 fatal("cannot happen, missing inline def %s", s);
 366
 367         return tmp;
 368 }
 369
 370 void
 371 c_state(Symbol *s, Symbol *t, Symbol *ival)     /* name, scope, ival */
 372 {       C_Added *r;
 373
 374         r = (C_Added *) emalloc(sizeof(C_Added));
 375         r->s = s;       /* pointer to a data object */
 376         r->t = t;       /* size of object, or "global", or "local proctype_name"  */
 377         r->ival = ival;
 378         r->lno = lineno;
 379         r->fnm = Fname;
 380         r->nxt = c_added;
 381
 382         if(strncmp(r->s->name, "\"unsigned unsigned", 18) == 0)
 383         {       int i;
 384                 for (i = 10; i < 18; i++)
 385                 {       r->s->name[i] = ' ';
 386                 }
 387         /*      printf("corrected <%s>\n", r->s->name); */
 388         }
 389         c_added = r;
 390 }
 391
 392 void
 393 c_track(Symbol *s, Symbol *t, Symbol *stackonly)        /* name, size */
 394 {       C_Added *r;
 395
 396         r = (C_Added *) emalloc(sizeof(C_Added));
 397         r->s = s;
 398         r->t = t;
 399         r->ival = stackonly;    /* abuse of name */
 400         r->nxt = c_tracked;
 401         r->fnm = Fname;
 402         r->lno = lineno;
 403         c_tracked = r;
 404
 405         if (stackonly != ZS)
 406         {       if (strcmp(stackonly->name, "\"Matched\"") == 0)
 407                         r->ival = ZS;   /* the default */
 408                 else if (strcmp(stackonly->name, "\"UnMatched\"") != 0
 409                      &&  strcmp(stackonly->name, "\"unMatched\"") != 0
 410                      &&  strcmp(stackonly->name, "\"StackOnly\"") != 0)
 411                         non_fatal("expecting '[Un]Matched', saw %s", stackonly->name);
 412                 else
 413                         has_stack = 1;  /* unmatched stack */
 414         }
 415 }
 416
 417 char *
 418 skip_white(char *p)
 419 {
 420         if (p != NULL)
 421         {       while (*p == ' ' || *p == '\t')
 422                         p++;
 423         } else
 424         {       fatal("bad format - 1", (char *) 0);
 425         }
 426         return p;
 427 }
 428
 429 char *
 430 skip_nonwhite(char *p)
 431 {
 432         if (p != NULL)
 433         {       while (*p != ' ' && *p != '\t')
 434                         p++;
 435         } else
 436         {       fatal("bad format - 2", (char *) 0);
 437         }
 438         return p;
 439 }
 440
 441 static char *
 442 jump_etc(C_Added *r)
 443 {       char *op = r->s->name;
 444         char *p = op;
 445         char *q = (char *) 0;
 446         int oln = lineno;
 447         Symbol *ofnm = Fname;
 448
 449         /* try to get the type separated from the name */
 450         lineno = r->lno;
 451         Fname  = r->fnm;
 452
 453         p = skip_white(p);      /* initial white space */
 454
 455         if (strncmp(p, "enum", strlen("enum")) == 0) /* special case: a two-part typename */
 456         {       p += strlen("enum")+1;
 457                 p = skip_white(p);
 458         }
 459         if (strncmp(p, "unsigned", strlen("unsigned")) == 0) /* possibly a two-part typename */
 460         {       p += strlen("unsigned")+1;
 461                 q = p = skip_white(p);
 462         }
 463         p = skip_nonwhite(p);   /* type name */
 464         p = skip_white(p);      /* white space */
 465         while (*p == '*') p++;  /* decorations */
 466         p = skip_white(p);      /* white space */
 467
 468         if (*p == '\0')
 469         {       if (q)
 470                 {       p = q;  /* unsigned with implied 'int' */
 471                 } else
 472                 {       fatal("c_state format (%s)", op);
 473         }       }
 474
 475         if (strchr(p, '[') && !strchr(p, '{'))
 476         {       non_fatal("array initialization error, c_state (%s)", p);
 477                 p = (char *) 0;
 478         }
 479
 480         lineno = oln;
 481         Fname = ofnm;
 482
 483         return p;
 484 }
 485
 486 void
 487 c_add_globinit(FILE *fd)
 488 {       C_Added *r;
 489         char *p, *q;
 490
 491         fprintf(fd, "void\nglobinit(void)\n{\n");
 492         for (r = c_added; r; r = r->nxt)
 493         {       if (r->ival == ZS)
 494                         continue;
 495
 496                 if (strncmp(r->t->name, " Global ", strlen(" Global ")) == 0)
 497                 {       for (q = r->ival->name; *q; q++)
 498                         {       if (*q == '\"')
 499                                         *q = ' ';
 500                                 if (*q == '\\')
 501                                         *q++ = ' '; /* skip over the next */
 502                         }
 503                         p = jump_etc(r);        /* e.g., "int **q" */
 504                         if (p)
 505                         fprintf(fd, "   now.%s = %s;\n", p, r->ival->name);
 506
 507                 } else
 508                 if (strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) == 0)
 509                 {       for (q = r->ival->name; *q; q++)
 510                         {       if (*q == '\"')
 511                                         *q = ' ';
 512                                 if (*q == '\\')
 513                                         *q++ = ' '; /* skip over the next */
 514                         }
 515                         p = jump_etc(r);        /* e.g., "int **q" */
 516                         if (p)
 517                         fprintf(fd, "   %s = %s;\n", p, r->ival->name); /* no now. prefix */
 518
 519         }       }
 520         fprintf(fd, "}\n");
 521 }
 522
 523 void
 524 c_add_locinit(FILE *fd, int tpnr, char *pnm)
 525 {       C_Added *r;
 526         char *p, *q, *s;
 527         int frst = 1;
 528
 529         fprintf(fd, "void\nlocinit%d(int h)\n{\n", tpnr);
 530         for (r = c_added; r; r = r->nxt)
 531                 if (r->ival != ZS
 532                 &&  strncmp(r->t->name, " Local", strlen(" Local")) == 0)
 533                 {       for (q = r->ival->name; *q; q++)
 534                                 if (*q == '\"')
 535                                         *q = ' ';
 536
 537                         p = jump_etc(r);        /* e.g., "int **q" */
 538
 539                         q = r->t->name + strlen(" Local");
 540                         while (*q == ' ' || *q == '\t')
 541                                 q++;                    /* process name */
 542
 543                         s = (char *) emalloc(strlen(q)+1);
 544                         strcpy(s, q);
 545
 546                         q = &s[strlen(s)-1];
 547                         while (*q == ' ' || *q == '\t')
 548                                 *q-- = '\0';
 549
 550                         if (strcmp(pnm, s) != 0)
 551                                 continue;
 552
 553                         if (frst)
 554                         {       fprintf(fd, "\tuchar *this = pptr(h);\n");
 555                                 frst = 0;
 556                         }
 557
 558                         if (p)
 559                         {       fprintf(fd, "\t\t((P%d *)this)->%s = %s;\n",
 560                                         tpnr, p, r->ival->name);
 561                         }
 562                 }
 563         fprintf(fd, "}\n");
 564 }
 565
 566 /* tracking:
 567         1. for non-global and non-local c_state decls: add up all the sizes in c_added
 568         2. add a global char array of that size into now
 569         3. generate a routine that memcpy's the required values into that array
 570         4. generate a call to that routine
 571  */
 572
 573 void
 574 c_preview(void)
 575 {       C_Added *r;
 576
 577         hastrack = 0;
 578         if (c_tracked)
 579                 hastrack = 1;
 580         else
 581         for (r = c_added; r; r = r->nxt)
 582                 if (strncmp(r->t->name, " Global ", strlen(" Global ")) != 0
 583                 &&  strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) != 0
 584                 &&  strncmp(r->t->name, " Local",  strlen(" Local"))  != 0)
 585                 {       hastrack = 1;   /* c_state variant now obsolete */
 586                         break;
 587                 }
 588 }
 589
 590 int
 591 c_add_sv(FILE *fd)      /* 1+2 -- called in pangen1.c */
 592 {       C_Added *r;
 593         int cnt = 0;
 594
 595         if (!c_added && !c_tracked) return 0;
 596
 597         for (r = c_added; r; r = r->nxt)        /* pickup global decls */
 598                 if (strncmp(r->t->name, " Global ", strlen(" Global ")) == 0)
 599                         fprintf(fd, "   %s;\n", r->s->name);
 600
 601         for (r = c_added; r; r = r->nxt)
 602                 if (strncmp(r->t->name, " Global ", strlen(" Global ")) != 0
 603                 &&  strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) != 0
 604                 &&  strncmp(r->t->name, " Local",  strlen(" Local"))  != 0)
 605                 {       cnt++;  /* obsolete use */
 606                 }
 607
 608         for (r = c_tracked; r; r = r->nxt)
 609                 cnt++;          /* preferred use */
 610
 611         if (cnt == 0) return 0;
 612
 613         cnt = 0;
 614         fprintf(fd, "   uchar c_state[");
 615         for (r = c_added; r; r = r->nxt)
 616                 if (strncmp(r->t->name, " Global ", strlen(" Global ")) != 0
 617                 &&  strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) != 0
 618                 &&  strncmp(r->t->name, " Local",  strlen(" Local"))  != 0)
 619                 {       fprintf(fd, "%ssizeof(%s)",
 620                                 (cnt==0)?"":"+", r->t->name);
 621                         cnt++;
 622                 }
 623
 624         for (r = c_tracked; r; r = r->nxt)
 625         {       if (r->ival != ZS) continue;
 626
 627                 fprintf(fd, "%s%s",
 628                         (cnt==0)?"":"+", r->t->name);
 629                 cnt++;
 630         }
 631
 632         if (cnt == 0) fprintf(fd, "4"); /* now redundant */
 633         fprintf(fd, "];\n");
 634         return 1;
 635 }
 636
 637 void
 638 c_stack_size(FILE *fd)
 639 {       C_Added *r;
 640         int cnt = 0;
 641
 642         for (r = c_tracked; r; r = r->nxt)
 643                 if (r->ival != ZS)
 644                 {       fprintf(fd, "%s%s",
 645                                 (cnt==0)?"":"+", r->t->name);
 646                         cnt++;
 647                 }
 648         if (cnt == 0)
 649         {       fprintf(fd, "WS");
 650         }
 651 }
 652
 653 void
 654 c_add_stack(FILE *fd)
 655 {       C_Added *r;
 656         int cnt = 0;
 657
 658         if ((!c_added && !c_tracked) || !has_stack)
 659         {       return;
 660         }
 661
 662         for (r = c_tracked; r; r = r->nxt)
 663                 if (r->ival != ZS)
 664                 {       cnt++;
 665                 }
 666
 667         if (cnt > 0)
 668         {       fprintf(fd, "   uchar c_stack[StackSize];\n");
 669         }
 670 }
 671
 672 void
 673 c_add_hidden(FILE *fd)
 674 {       C_Added *r;
 675
 676         for (r = c_added; r; r = r->nxt)        /* pickup hidden decls */
 677                 if (strncmp(r->t->name, "\"Hidden\"", strlen("\"Hidden\"")) == 0)
 678                 {       r->s->name[strlen(r->s->name)-1] = ' ';
 679                         fprintf(fd, "%s;        /* Hidden */\n", &r->s->name[1]);
 680                         r->s->name[strlen(r->s->name)-1] = '"';
 681                 }
 682         /* called before c_add_def - quotes are still there */
 683 }
 684
 685 void
 686 c_add_loc(FILE *fd, char *s)    /* state vector entries for proctype s */
 687 {       C_Added *r;
 688         static char buf[1024];
 689         char *p;
 690
 691         if (!c_added) return;
 692
 693         strcpy(buf, s);
 694         strcat(buf, " ");
 695         for (r = c_added; r; r = r->nxt)        /* pickup local decls */
 696                 if (strncmp(r->t->name, " Local", strlen(" Local")) == 0)
 697                 {       p = r->t->name + strlen(" Local");
 698 fprintf(fd, "/* XXX p=<%s>, s=<%s>, buf=<%s> r->s->name=<%s>XXX */\n", p, s, buf, r->s->name);
 699                         while (*p == ' ' || *p == '\t')
 700                                 p++;
 701                         if (strcmp(p, buf) == 0)
 702                                 fprintf(fd, "   %s;\n", r->s->name);
 703                 }
 704 }
 705 void
 706 c_add_def(FILE *fd)     /* 3 - called in plunk_c_fcts() */
 707 {       C_Added *r;
 708
 709         fprintf(fd, "#if defined(C_States) && (HAS_TRACK==1)\n");
 710         for (r = c_added; r; r = r->nxt)
 711         {       r->s->name[strlen(r->s->name)-1] = ' ';
 712                 r->s->name[0] = ' '; /* remove the "s */
 713
 714                 r->t->name[strlen(r->t->name)-1] = ' ';
 715                 r->t->name[0] = ' ';
 716
 717                 if (strncmp(r->t->name, " Global ", strlen(" Global ")) == 0
 718                 ||  strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) == 0
 719                 ||  strncmp(r->t->name, " Local",  strlen(" Local"))  == 0)
 720                         continue;
 721
 722                 if (strchr(r->s->name, '&'))
 723                         fatal("dereferencing state object: %s", r->s->name);
 724
 725                 fprintf(fd, "extern %s %s;\n", r->t->name, r->s->name);
 726         }
 727         for (r = c_tracked; r; r = r->nxt)
 728         {       r->s->name[strlen(r->s->name)-1] = ' ';
 729                 r->s->name[0] = ' '; /* remove " */
 730
 731                 r->t->name[strlen(r->t->name)-1] = ' ';
 732                 r->t->name[0] = ' ';
 733         }
 734
 735         if (separate == 2)
 736         {       fprintf(fd, "#endif\n");
 737                 return;
 738         }
 739
 740         if (has_stack)
 741         {       fprintf(fd, "int cpu_printf(const char *, ...);\n");
 742                 fprintf(fd, "void\nc_stack(uchar *p_t_r)\n{\n");
 743                 fprintf(fd, "#ifdef VERBOSE\n");
 744                 fprintf(fd, "   cpu_printf(\"c_stack %%u\\n\", p_t_r);\n");
 745                 fprintf(fd, "#endif\n");
 746                 for (r = c_tracked; r; r = r->nxt)
 747                 {       if (r->ival == ZS) continue;
 748
 749                         fprintf(fd, "\tif(%s)\n", r->s->name);
 750                         fprintf(fd, "\t\tmemcpy(p_t_r, %s, %s);\n",
 751                                 r->s->name, r->t->name);
 752                         fprintf(fd, "\telse\n");
 753                         fprintf(fd, "\t\tmemset(p_t_r, 0, %s);\n",
 754                                 r->t->name);
 755                         fprintf(fd, "\tp_t_r += %s;\n", r->t->name);
 756                 }
 757                 fprintf(fd, "}\n\n");
 758         }
 759
 760         fprintf(fd, "void\nc_update(uchar *p_t_r)\n{\n");
 761         fprintf(fd, "#ifdef VERBOSE\n");
 762         fprintf(fd, "   printf(\"c_update %%p\\n\", p_t_r);\n");
 763         fprintf(fd, "#endif\n");
 764         for (r = c_added; r; r = r->nxt)
 765         {       if (strncmp(r->t->name, " Global ", strlen(" Global ")) == 0
 766                 ||  strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) == 0
 767                 ||  strncmp(r->t->name, " Local",  strlen(" Local"))  == 0)
 768                         continue;
 769
 770                 fprintf(fd, "\tmemcpy(p_t_r, &%s, sizeof(%s));\n",
 771                         r->s->name, r->t->name);
 772                 fprintf(fd, "\tp_t_r += sizeof(%s);\n", r->t->name);
 773         }
 774
 775         for (r = c_tracked; r; r = r->nxt)
 776         {       if (r->ival) continue;
 777
 778                 fprintf(fd, "\tif(%s)\n", r->s->name);
 779                 fprintf(fd, "\t\tmemcpy(p_t_r, %s, %s);\n",
 780                         r->s->name, r->t->name);
 781                 fprintf(fd, "\telse\n");
 782                 fprintf(fd, "\t\tmemset(p_t_r, 0, %s);\n",
 783                         r->t->name);
 784                 fprintf(fd, "\tp_t_r += %s;\n", r->t->name);
 785         }
 786
 787         fprintf(fd, "}\n");
 788
 789         if (has_stack)
 790         {       fprintf(fd, "void\nc_unstack(uchar *p_t_r)\n{\n");
 791                 fprintf(fd, "#ifdef VERBOSE\n");
 792                 fprintf(fd, "   cpu_printf(\"c_unstack %%u\\n\", p_t_r);\n");
 793                 fprintf(fd, "#endif\n");
 794                 for (r = c_tracked; r; r = r->nxt)
 795                 {       if (r->ival == ZS) continue;
 796
 797                         fprintf(fd, "\tif(%s)\n", r->s->name);
 798                         fprintf(fd, "\t\tmemcpy(%s, p_t_r, %s);\n",
 799                                 r->s->name, r->t->name);
 800                         fprintf(fd, "\tp_t_r += %s;\n", r->t->name);
 801                 }
 802                 fprintf(fd, "}\n");
 803         }
 804
 805         fprintf(fd, "void\nc_revert(uchar *p_t_r)\n{\n");
 806         fprintf(fd, "#ifdef VERBOSE\n");
 807         fprintf(fd, "   printf(\"c_revert %%p\\n\", p_t_r);\n");
 808         fprintf(fd, "#endif\n");
 809         for (r = c_added; r; r = r->nxt)
 810         {       if (strncmp(r->t->name, " Global ", strlen(" Global ")) == 0
 811                 ||  strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) == 0
 812                 ||  strncmp(r->t->name, " Local",  strlen(" Local"))  == 0)
 813                         continue;
 814
 815                 fprintf(fd, "\tmemcpy(&%s, p_t_r, sizeof(%s));\n",
 816                         r->s->name, r->t->name);
 817                 fprintf(fd, "\tp_t_r += sizeof(%s);\n", r->t->name);
 818         }
 819         for (r = c_tracked; r; r = r->nxt)
 820         {       if (r->ival != ZS) continue;
 821
 822                 fprintf(fd, "\tif(%s)\n", r->s->name);
 823                 fprintf(fd, "\t\tmemcpy(%s, p_t_r, %s);\n",
 824                         r->s->name, r->t->name);
 825                 fprintf(fd, "\tp_t_r += %s;\n", r->t->name);
 826         }
 827
 828         fprintf(fd, "}\n");
 829         fprintf(fd, "#endif\n");
 830 }
 831
 832 void
 833 plunk_reverse(FILE *fd, IType *p, int matchthis)
 834 {       char *y, *z;
 835
 836         if (!p) return;
 837         plunk_reverse(fd, p->nxt, matchthis);
 838
 839         if (!p->nm->context
 840         &&   p->nm->type == matchthis
 841         &&   p->is_expr == 0)
 842         {       fprintf(fd, "\n/* start of %s */\n", p->nm->name);
 843                 z = (char *) p->cn;
 844                 while (*z == '\n' || *z == '\r' || *z == '\\')
 845                 {       z++;
 846                 }
 847                 /* e.g.: \#include "..." */
 848
 849                 y = z;
 850                 while ((y = strstr(y, "\\#")) != NULL)
 851                 {       *y = '\n'; y++;
 852                 }
 853
 854                 fprintf(fd, "%s\n", z);
 855                 fprintf(fd, "\n/* end of %s */\n", p->nm->name);
 856         }
 857 }
 858
 859 void
 860 plunk_c_decls(FILE *fd)
 861 {
 862         plunk_reverse(fd, seqnames, CODE_DECL);
 863 }
 864
 865 void
 866 plunk_c_fcts(FILE *fd)
 867 {
 868         if (separate == 2 && hastrack)
 869         {       c_add_def(fd);
 870                 return;
 871         }
 872
 873         c_add_hidden(fd);
 874         plunk_reverse(fd, seqnames, CODE_FRAG);
 875
 876         if (c_added || c_tracked)       /* enables calls to c_revert and c_update */
 877                 fprintf(fd, "#define C_States   1\n");
 878         else
 879                 fprintf(fd, "#undef C_States\n");
 880
 881         if (hastrack)
 882                 c_add_def(fd);
 883
 884         c_add_globinit(fd);
 885         do_locinits(fd);
 886 }
 887
 888 static void
 889 check_inline(IType *tmp)
 890 {       char buf[128];
 891         ProcList *p;
 892
 893         if (!X) return;
 894
 895         for (p = rdy; p; p = p->nxt)
 896         {       if (strcmp(p->n->name, X->n->name) == 0)
 897                         continue;
 898                 sprintf(buf, "P%s->", p->n->name);
 899                 if (strstr((char *)tmp->cn, buf))
 900                 {       printf("spin: in proctype %s, ref to object in proctype %s\n",
 901                                 X->n->name, p->n->name);
 902                         fatal("invalid variable ref in '%s'", tmp->nm->name);
 903         }       }
 904 }
 905
 906 extern short terse;
 907 extern short nocast;
 908
 909 void
 910 plunk_expr(FILE *fd, char *s)
 911 {       IType *tmp;
 912         char *q;
 913
 914         tmp = find_inline(s);
 915         check_inline(tmp);
 916
 917         if (terse && nocast)
 918         {       for (q = (char *) tmp->cn; q && *q != '\0'; q++)
 919                 {       fflush(fd);
 920                         if (*q == '"')
 921                         {       fprintf(fd, "\\");
 922                         }
 923                         fprintf(fd, "%c", *q);
 924                 }
 925         } else
 926         {       fprintf(fd, "%s", (char *) tmp->cn);
 927         }
 928 }
 929
 930 void
 931 preruse(FILE *fd, Lextok *n)    /* check a condition for c_expr with preconditions */
 932 {       IType *tmp;
 933
 934         if (!n) return;
 935         if (n->ntyp == C_EXPR)
 936         {       tmp = find_inline(n->sym->name);
 937                 if (tmp->prec)
 938                 {       fprintf(fd, "if (!(%s)) { if (!readtrail) { depth++; ", tmp->prec);
 939                         fprintf(fd, "trpt++; trpt->pr = II; trpt->o_t = t; trpt->st = tt; ");
 940                         fprintf(fd, "uerror(\"c_expr line %d precondition false: %s\"); continue;",
 941                                 tmp->dln, tmp->prec);
 942                         fprintf(fd, " } else { printf(\"pan: precondition false: %s\\n\"); ",
 943                                 tmp->prec);
 944                         fprintf(fd, "_m = 3; goto P999; } } \n\t\t");
 945                 }
 946         } else
 947         {       preruse(fd, n->rgt);
 948                 preruse(fd, n->lft);
 949         }
 950 }
 951
 952 int
 953 glob_inline(char *s)
 954 {       IType *tmp;
 955         char *bdy;
 956
 957         tmp = find_inline(s);
 958         bdy = (char *) tmp->cn;
 959         return (strstr(bdy, "now.")             /* global ref or   */
 960         ||      strchr(bdy, '(') > bdy);        /* possible C-function call */
 961 }
 962
 963 char *
 964 put_inline(FILE *fd, char *s)
 965 {       IType *tmp;
 966
 967         tmp = find_inline(s);
 968         check_inline(tmp);
 969         return (char *) tmp->cn;
 970 }
 971
 972 void
 973 mark_last(void)
 974 {
 975         if (seqnames)
 976         {       seqnames->is_expr = 1;
 977         }
 978 }
 979
 980 void
 981 plunk_inline(FILE *fd, char *s, int how, int gencode)   /* c_code with precondition */
 982 {       IType *tmp;
 983
 984         tmp = find_inline(s);
 985         check_inline(tmp);
 986
 987         fprintf(fd, "{ ");
 988         if (how && tmp->prec)
 989         {       fprintf(fd, "if (!(%s)) { if (!readtrail) {",
 990                         tmp->prec);
 991                 fprintf(fd, " uerror(\"c_code line %d precondition false: %s\"); continue; ",
 992                         tmp->dln,
 993                         tmp->prec);
 994                 fprintf(fd, "} else { ");
 995                 fprintf(fd, "printf(\"pan: precondition false: %s\\n\"); _m = 3; goto P999; } } ",
 996                         tmp->prec);
 997         }
 998
 999         if (!gencode)   /* not in d_step */
1000         {       fprintf(fd, "\n\t\tsv_save();");
1001         }
1002
1003         fprintf(fd, "%s", (char *) tmp->cn);
1004         fprintf(fd, " }\n");
1005 }
1006
1007 int
1008 side_scan(char *t, char *pat)
1009 {       char *r = strstr(t, pat);
1010         return (r
1011                 && *(r-1) != '"'
1012                 && *(r-1) != '\'');
1013 }
1014
1015 void
1016 no_side_effects(char *s)
1017 {       IType *tmp;
1018         char *t;
1019
1020         /* could still defeat this check via hidden
1021          * side effects in function calls,
1022          * but this will catch at least some cases
1023          */
1024
1025         tmp = find_inline(s);
1026         t = (char *) tmp->cn;
1027
1028         if (side_scan(t, ";")
1029         ||  side_scan(t, "++")
1030         ||  side_scan(t, "--"))
1031         {
1032 bad:            lineno = tmp->dln;
1033                 Fname = tmp->dfn;
1034                 non_fatal("c_expr %s has side-effects", s);
1035                 return;
1036         }
1037         while ((t = strchr(t, '=')) != NULL)
1038         {       if (*(t-1) == '!'
1039                 ||  *(t-1) == '>'
1040                 ||  *(t-1) == '<'
1041                 ||  *(t-1) == '"'
1042                 ||  *(t-1) == '\'')
1043                 {       t += 2;
1044                         continue;
1045                 }
1046                 t++;
1047                 if (*t != '=')
1048                         goto bad;
1049                 t++;
1050         }
1051 }
1052
1053 void
1054 pickup_inline(Symbol *t, Lextok *apars, Lextok *rval)
1055 {       IType *tmp; Lextok *p, *q; int j;
1056
1057         tmp = find_inline(t->name);
1058
1059         if (++Inlining >= MAXINL)
1060                 fatal("inlines nested too deeply", 0);
1061         tmp->cln = lineno;      /* remember calling point */
1062         tmp->cfn = Fname;       /* and filename */
1063         tmp->rval = rval;
1064
1065         for (p = apars, q = tmp->params, j = 0; p && q; p = p->rgt, q = q->rgt)
1066                 j++; /* count them */
1067         if (p || q)
1068                 fatal("wrong nr of params on call of '%s'", t->name);
1069
1070         tmp->anms  = (char **) emalloc(j * sizeof(char *));
1071         for (p = apars, j = 0; p; p = p->rgt, j++)
1072         {       tmp->anms[j] = (char *) emalloc(strlen(IArg_cont[j])+1);
1073                 strcpy(tmp->anms[j], IArg_cont[j]);
1074         }
1075
1076         lineno = tmp->dln;      /* linenr of def */
1077         Fname = tmp->dfn;       /* filename of same */
1078         Inliner[Inlining] = (char *)tmp->cn;
1079         Inline_stub[Inlining] = tmp;
1080 #if 0
1081         if (verbose&32)
1082         printf("spin: %s:%d, inlining '%s' (from %s:%d)\n",
1083                 tmp->cfn->name, tmp->cln, t->name, tmp->dfn->name, tmp->dln);
1084 #endif
1085         for (j = 0; j < Inlining; j++)
1086         {       if (Inline_stub[j] == Inline_stub[Inlining])
1087                 {       fatal("cyclic inline attempt on: %s", t->name);
1088         }       }
1089         last_token = SEMI;      /* avoid insertion of extra semi */
1090 }
1091
1092 extern int pp_mode;
1093
1094 static void
1095 do_directive(int first)
1096 {       int c = first;  /* handles lines starting with pound */
1097
1098         getword(c, isalpha_);
1099
1100         if (strcmp(yytext, "#ident") == 0)
1101                 goto done;
1102
1103         if ((c = Getchar()) != ' ')
1104                 fatal("malformed preprocessor directive - # .", 0);
1105
1106         if (!isdigit_(c = Getchar()))
1107                 fatal("malformed preprocessor directive - # .lineno", 0);
1108
1109         getword(c, isdigit_);
1110         lineno = atoi(yytext);  /* pickup the line number */
1111
1112         if ((c = Getchar()) == '\n')
1113                 return; /* no filename */
1114
1115         if (c != ' ')
1116                 fatal("malformed preprocessor directive - .fname", 0);
1117
1118         if ((c = Getchar()) != '\"')
1119         {       printf("got %c, expected \" -- lineno %d\n", c, lineno);
1120                 fatal("malformed preprocessor directive - .fname (%s)", yytext);
1121         }
1122
1123         getword(Getchar(), notquote);   /* was getword(c, notquote); */
1124         if (Getchar() != '\"')
1125                 fatal("malformed preprocessor directive - fname.", 0);
1126
1127         /* strcat(yytext, "\""); */
1128         Fname = lookup(yytext);
1129 done:
1130         while (Getchar() != '\n')
1131                 ;
1132 }
1133
1134 void
1135 precondition(char *q)
1136 {       int c, nest = 1;
1137
1138         for (;;)
1139         {       c = Getchar();
1140                 *q++ = c;
1141                 switch (c) {
1142                 case '\n':
1143                         lineno++;
1144                         break;
1145                 case '[':
1146                         nest++;
1147                         break;
1148                 case ']':
1149                         if (--nest <= 0)
1150                         {       *--q = '\0';
1151                                 return;
1152                         }
1153                         break;
1154                 }
1155         }
1156         fatal("cannot happen", (char *) 0); /* unreachable */
1157 }
1158
1159
1160 Symbol *
1161 prep_inline(Symbol *s, Lextok *nms)
1162 {       int c, nest = 1, dln, firstchar, cnr;
1163         char *p;
1164         Lextok *t;
1165         static char Buf1[SOMETHINGBIG], Buf2[RATHERSMALL];
1166         static int c_code = 1;
1167
1168         for (t = nms; t; t = t->rgt)
1169                 if (t->lft)
1170                 {       if (t->lft->ntyp != NAME)
1171                         fatal("bad param to inline %s", s?s->name:"--");
1172                         t->lft->sym->hidden |= 32;
1173                 }
1174
1175         if (!s) /* C_Code fragment */
1176         {       s = (Symbol *) emalloc(sizeof(Symbol));
1177                 s->name = (char *) emalloc(strlen("c_code")+26);
1178                 sprintf(s->name, "c_code%d", c_code++);
1179                 s->context = context;
1180                 s->type = CODE_FRAG;
1181         } else
1182         {       s->type = PREDEF;
1183         }
1184
1185         p = &Buf1[0];
1186         Buf2[0] = '\0';
1187         for (;;)
1188         {       c = Getchar();
1189                 switch (c) {
1190                 case '[':
1191                         if (s->type != CODE_FRAG)
1192                                 goto bad;
1193                         precondition(&Buf2[0]); /* e.g., c_code [p] { r = p-r; } */
1194                         continue;
1195                 case '{':
1196                         break;
1197                 case '\n':
1198                         lineno++;
1199                         /* fall through */
1200                 case ' ': case '\t': case '\f': case '\r':
1201                         continue;
1202                 default :
1203                          printf("spin: saw char '%c'\n", c);
1204 bad:                     fatal("bad inline: %s", s->name);
1205                 }
1206                 break;
1207         }
1208         dln = lineno;
1209         if (s->type == CODE_FRAG)
1210         {       if (verbose&32)
1211                 {       sprintf(Buf1, "\t/* line %d %s */\n\t\t",
1212                                 lineno, Fname->name);
1213                 } else
1214                 {       strcpy(Buf1, "");
1215                 }
1216         } else
1217         {       sprintf(Buf1, "\n#line %d \"%s\"\n{", lineno, Fname->name);
1218         }
1219         p += strlen(Buf1);
1220         firstchar = 1;
1221
1222         cnr = 1; /* not zero */
1223 more:
1224         c = Getchar();
1225         *p++ = (char) c;
1226         if (p - Buf1 >= SOMETHINGBIG)
1227                 fatal("inline text too long", 0);
1228         switch (c) {
1229         case '\n':
1230                 lineno++;
1231                 cnr = 0;
1232                 break;
1233         case '{':
1234                 cnr++;
1235                 nest++;
1236                 break;
1237         case '}':
1238                 cnr++;
1239                 if (--nest <= 0)
1240                 {       *p = '\0';
1241                         if (s->type == CODE_FRAG)
1242                         {       *--p = '\0';    /* remove trailing '}' */
1243                         }
1244                         def_inline(s, dln, &Buf1[0], &Buf2[0], nms);
1245                         if (firstchar)
1246                         {       printf("%3d: %s, warning: empty inline definition (%s)\n",
1247                                         dln, Fname->name, s->name);
1248                         }
1249                         return s;       /* normal return */
1250                 }
1251                 break;
1252         case '#':
1253                 if (cnr == 0)
1254                 {       p--;
1255                         do_directive(c); /* reads to newline */
1256                 } else
1257                 {       firstchar = 0;
1258                         cnr++;
1259                 }
1260                 break;
1261         case '\t':
1262         case ' ':
1263         case '\f':
1264                 cnr++;
1265                 break;
1266         case '"':
1267                 do {
1268                         c = Getchar();
1269                         *p++ = (char) c;
1270                         if (c == '\\')
1271                         {       *p++ = (char) Getchar();
1272                         }
1273                         if (p - Buf1 >= SOMETHINGBIG)
1274                         {       fatal("inline text too long", 0);
1275                         }
1276                 } while (c != '"');     /* end of string */
1277                 /* *p = '\0'; */
1278                 break;
1279         case '\'':
1280                 c = Getchar();
1281                 *p++ = (char) c;
1282                 if (c == '\\')
1283                 {       *p++ = (char) Getchar();
1284                 }
1285                 c = Getchar();
1286                 *p++ = (char) c;
1287                 assert(c == '\'');
1288                 break;
1289         default:
1290                 firstchar = 0;
1291                 cnr++;
1292                 break;
1293         }
1294         goto more;
1295 }
1296
1297 static void
1298 set_cur_scope(void)
1299 {       int i;
1300         char tmpbuf[256];
1301
1302         strcpy(CurScope, "_");
1303
1304         if (context)
1305         for (i = 0; i < scope_level; i++)
1306         {       sprintf(tmpbuf, "%d_", scope_seq[i]);
1307                 strcat(CurScope, tmpbuf);
1308         }
1309 }
1310
1311 static int
1312 pre_proc(void)
1313 {       char b[512];
1314         int c, i = 0;
1315
1316         b[i++] = '#';
1317         while ((c = Getchar()) != '\n' && c != EOF)
1318         {       b[i++] = (char) c;
1319         }
1320         b[i] = '\0';
1321         yylval = nn(ZN, 0, ZN, ZN);
1322         yylval->sym = lookup(b);
1323         return PREPROC;
1324 }
1325
1326 static int specials[] = {
1327         '}', ')', ']',
1328         OD, FI, ELSE, BREAK,
1329         C_CODE, C_EXPR, C_DECL,
1330         NAME, CONST, INCR, DECR, 0
1331 };
1332
1333 int
1334 follows_token(int c)
1335 {       int i;
1336
1337         for (i = 0; specials[i]; i++)
1338         {       if (c == specials[i])
1339                 {       return 1;
1340         }       }
1341         return 0;
1342 }
1343 #define DEFER_LTL
1344 #ifdef DEFER_LTL
1345 /* defer ltl formula to the end of the spec
1346  * no matter where they appear in the original
1347  */
1348
1349 static int deferred = 0;
1350 static FILE *defer_fd;
1351
1352 int
1353 get_deferred(void)
1354 {
1355         if (!defer_fd)
1356         {       return 0;       /* nothing was deferred */
1357         }
1358         fclose(defer_fd);
1359
1360         defer_fd = fopen(TMP_FILE2, "r");
1361         if (!defer_fd)
1362         {       non_fatal("cannot retrieve deferred ltl formula", (char *) 0);
1363                 return 0;
1364         }
1365         fclose(yyin);
1366         yyin = defer_fd;
1367         return 1;
1368 }
1369
1370 void
1371 zap_deferred(void)
1372 {
1373         (void) unlink(TMP_FILE2);
1374 }
1375
1376 int
1377 put_deferred(void)
1378 {       int c, cnt;
1379         if (!defer_fd)
1380         {       defer_fd = fopen(TMP_FILE2, "w+");
1381                 if (!defer_fd)
1382                 {       non_fatal("cannot defer ltl expansion", (char *) 0);
1383                         return 0;
1384         }       }
1385         fprintf(defer_fd, "ltl ");
1386         cnt = 0;
1387         while ((c = getc(yyin)) != EOF)
1388         {       if (c == '{')
1389                 {       cnt++;
1390                 }
1391                 if (c == '}')
1392                 {       cnt--;
1393                         if (cnt == 0)
1394                         {       break;
1395                 }       }
1396                 fprintf(defer_fd, "%c", c);
1397         }
1398         fprintf(defer_fd, "}\n");
1399         fflush(defer_fd);
1400         return 1;
1401 }
1402 #endif
1403
1404 #define EXPAND_SELECT
1405 #ifdef EXPAND_SELECT
1406 static char tmp_hold[256];
1407 static int  tmp_has;
1408
1409 void
1410 new_select(void)
1411 {       tmp_hold[0] = '\0';
1412         tmp_has = 0;
1413 }
1414
1415 int
1416 scan_to(int stop, int (*tst)(int), char *buf)
1417 {       int c, i = 0;
1418
1419         do {    c = Getchar();
1420                 if (tmp_has < sizeof(tmp_hold))
1421                 {       tmp_hold[tmp_has++] = c;
1422                 }
1423                 if (c == '\n')
1424                 {       lineno++;
1425                 } else if (buf)
1426                 {       buf[i++] = c;
1427                 }
1428                 if (tst && !tst(c) && c != ' ' && c != '\t')
1429                 {       break;
1430                 }
1431         } while (c != stop && c != EOF);
1432
1433         if (buf)
1434         {       buf[i-1] = '\0';
1435         }
1436
1437         if (c != stop)
1438         {       if (0)
1439                 {       printf("saw: '%c', expected '%c'\n", c, stop);
1440                 }
1441                 if (tmp_has < sizeof(tmp_hold))
1442                 {       tmp_hold[tmp_has] = '\0';
1443                         push_back(tmp_hold);
1444                         if (0)
1445                         {       printf("pushed back: <'%s'>\n", tmp_hold);
1446                         }
1447                         return 0; /* internal expansion fails */
1448                 } else
1449                 {       fatal("expecting select ( name : constant .. constant )", 0);
1450         }       }
1451         return 1;               /* success */
1452 }
1453 #endif
1454
1455 int
1456 lex(void)
1457 {       int c;
1458 again:
1459         c = Getchar();
1460         yytext[0] = (char) c;
1461         yytext[1] = '\0';
1462         switch (c) {
1463         case EOF:
1464 #ifdef DEFER_LTL
1465                 if (!deferred)
1466                 {       deferred = 1;
1467                         if (get_deferred())
1468                         {       goto again;
1469                         }
1470                 } else
1471                 {       zap_deferred();
1472                 }
1473 #endif
1474                 return c;
1475         case '\n':              /* newline */
1476                 lineno++;
1477                 /* make most semi-colons optional */
1478                 if (implied_semis
1479         /*      &&  context     */
1480                 &&  in_seq
1481                 &&  par_cnt == 0
1482                 &&  follows_token(last_token))
1483                 {       if (0)
1484                         {       printf("insert ; line %d, last_token %d in_seq %d\n",
1485                                  lineno-1, last_token, in_seq);
1486                         }
1487                         ValToken(1, SEMI);
1488                 }
1489                 /* else fall thru */
1490         case '\r':              /* carriage return */
1491                 goto again;
1492
1493         case  ' ': case '\t': case '\f':        /* white space */
1494                 goto again;
1495
1496         case '#':               /* preprocessor directive */
1497                 if (in_comment) goto again;
1498                 if (pp_mode)
1499                 {       last_token = PREPROC;
1500                         return pre_proc();
1501                 }
1502                 do_directive(c);
1503                 goto again;
1504
1505         case '\"':
1506                 getword(c, notquote);
1507                 if (Getchar() != '\"')
1508                         fatal("string not terminated", yytext);
1509                 strcat(yytext, "\"");
1510                 SymToken(lookup(yytext), STRING)
1511
1512         case '$':
1513                 getword('\"', notdollar);
1514                 if (Getchar() != '$')
1515                         fatal("ltl definition not terminated", yytext);
1516                 strcat(yytext, "\"");
1517                 SymToken(lookup(yytext), STRING)
1518
1519         case '\'':      /* new 3.0.9 */
1520                 c = Getchar();
1521                 if (c == '\\')
1522                 {       c = Getchar();
1523                         if (c == 'n') c = '\n';
1524                         else if (c == 'r') c = '\r';
1525                         else if (c == 't') c = '\t';
1526                         else if (c == 'f') c = '\f';
1527                 }
1528                 if (Getchar() != '\'' && !in_comment)
1529                         fatal("character quote missing: %s", yytext);
1530                 ValToken(c, CONST)
1531
1532         default:
1533                 break;
1534         }
1535
1536         if (isdigit_(c))
1537         {       long int nr;
1538                 getword(c, isdigit_);
1539                 errno = 0;
1540                 nr = strtol(yytext, NULL, 10);
1541                 if (errno != 0)
1542                 {       fprintf(stderr, "spin: value out of range: '%s' read as '%d'\n",
1543                                 yytext, (int) nr);
1544                 }
1545                 ValToken((int)nr, CONST)
1546         }
1547
1548         if (isalpha_(c) || c == '_')
1549         {       getword(c, isalnum_);
1550                 if (!in_comment)
1551                 {       c = check_name(yytext);
1552
1553 #ifdef EXPAND_SELECT
1554                         if (c == SELECT && Inlining < 0)
1555                         {       char name[64], from[32], upto[32];
1556                                 int i, a, b;
1557                                 new_select();
1558                                 if (!scan_to('(', 0, 0)
1559                                 ||  !scan_to(':', isalnum, name)
1560                                 ||  !scan_to('.', isdigit, from)
1561                                 ||  !scan_to('.', 0, 0)
1562                                 ||  !scan_to(')', isdigit, upto))
1563                                 {       goto not_expanded;
1564                                 }
1565                                 a = atoi(from);
1566                                 b = atoi(upto);
1567                                 if (0)
1568                                 {       printf("Select %s from %d to %d\n",
1569                                                 name, a, b);
1570                                 }
1571                                 if (a > b)
1572                                 {       non_fatal("bad range in select statement", 0);
1573                                         goto again;
1574                                 }
1575                                 if (b - a <= 32)
1576                                 {       push_back("if ");
1577                                         for (i = a; i <= b; i++)
1578                                         {       char buf[128];
1579                                                 push_back(":: ");
1580                                                 sprintf(buf, "%s = %d ",
1581                                                         name, i);
1582                                                 push_back(buf);
1583                                         }
1584                                         push_back("fi ");
1585                                 } else
1586                                 {       char buf[128];
1587                                         sprintf(buf, "%s = %d; do ",
1588                                                 name, a);
1589                                         push_back(buf);
1590                                         sprintf(buf, ":: (%s < %d) -> %s++ ",
1591                                                 name, b, name);
1592                                         push_back(buf);
1593                                         push_back(":: break od; ");
1594                                 }
1595                                 goto again;
1596                         }
1597 not_expanded:
1598 #endif
1599
1600 #ifdef DEFER_LTL
1601                         if (c == LTL && !deferred)
1602                         {       if (put_deferred())
1603                                 {       goto again;
1604                         }       }
1605 #endif
1606                         if (c)
1607                         {       last_token = c;
1608                                 return c;
1609                         }
1610                         /* else fall through */
1611                 }
1612                 goto again;
1613         }
1614
1615         if (ltl_mode)
1616         {       switch (c) {
1617                 case '-': c = follow('>', IMPLIES,    '-'); break;
1618                 case '[': c = follow(']', ALWAYS,     '['); break;
1619                 case '<': c = follow('>', EVENTUALLY, '<');
1620                           if (c == '<')
1621                           {     c = Getchar();
1622                                 if (c == '-')
1623                                 {       c = follow('>', EQUIV, '-');
1624                                         if (c == '-')
1625                                         {       Ungetch(c);
1626                                                 c = '<';
1627                                         }
1628                                 } else
1629                                 {       Ungetch(c);
1630                                         c = '<';
1631                           }     }
1632                 default:  break;
1633         }       }
1634
1635         switch (c) {
1636         case '/': c = follow('*', 0, '/');
1637                   if (!c) { in_comment = 1; goto again; }
1638                   break;
1639         case '*': c = follow('/', 0, '*');
1640                   if (!c) { in_comment = 0; goto again; }
1641                   break;
1642         case ':': c = follow(':', SEP, ':'); break;
1643         case '-': c = follow('>', ARROW, follow('-', DECR, '-')); break;
1644         case '+': c = follow('+', INCR, '+'); break;
1645         case '<': c = follow('<', LSHIFT, follow('=', LE, LT)); break;
1646         case '>': c = follow('>', RSHIFT, follow('=', GE, GT)); break;
1647         case '=': c = follow('=', EQ, ASGN); break;
1648         case '!': c = follow('=', NE, follow('!', O_SND, SND)); break;
1649         case '?': c = follow('?', R_RCV, RCV); break;
1650         case '&': c = follow('&', AND, '&'); break;
1651         case '|': c = follow('|', OR, '|'); break;
1652         case ';': c = SEMI; break;
1653         case '.': c = follow('.', DOTDOT, '.'); break;
1654         case '{': scope_seq[scope_level++]++; set_cur_scope(); break;
1655         case '}': scope_level--; set_cur_scope(); break;
1656         default : break;
1657         }
1658         ValToken(0, c)
1659 }
1660
1661 static struct {
1662         char *s;        int tok;
1663 } LTL_syms[] = {
1664         /* [], <>, ->, and <-> are intercepted in lex() */
1665         { "U",          UNTIL   },
1666         { "V",          RELEASE },
1667         { "W",          WEAK_UNTIL },
1668         { "X",          NEXT    },
1669         { "always",     ALWAYS  },
1670         { "eventually", EVENTUALLY },
1671         { "until",      UNTIL   },
1672         { "stronguntil",UNTIL   },
1673         { "weakuntil",  WEAK_UNTIL   },
1674         { "release",    RELEASE },
1675         { "next",       NEXT    },
1676         { "implies",    IMPLIES },
1677         { "equivalent", EQUIV   },
1678         { 0,            0       },
1679 };
1680
1681 static struct {
1682         char *s;        int tok;        int val;        char *sym;
1683 } Names[] = {
1684         {"active",      ACTIVE,         0,              0},
1685         {"assert",      ASSERT,         0,              0},
1686         {"atomic",      ATOMIC,         0,              0},
1687         {"bit",         TYPE,           BIT,            0},
1688         {"bool",        TYPE,           BIT,            0},
1689         {"break",       BREAK,          0,              0},
1690         {"byte",        TYPE,           BYTE,           0},
1691         {"c_code",      C_CODE,         0,              0},
1692         {"c_decl",      C_DECL,         0,              0},
1693         {"c_expr",      C_EXPR,         0,              0},
1694         {"c_state",     C_STATE,        0,              0},
1695         {"c_track",     C_TRACK,        0,              0},
1696         {"D_proctype",  D_PROCTYPE,     0,              0},
1697         {"do",          DO,             0,              0},
1698         {"chan",        TYPE,           CHAN,           0},
1699         {"else",        ELSE,           0,              0},
1700         {"empty",       EMPTY,          0,              0},
1701         {"enabled",     ENABLED,        0,              0},
1702         {"eval",        EVAL,           0,              0},
1703         {"false",       CONST,          0,              0},
1704         {"fi",          FI,             0,              0},
1705         {"for",         FOR,            0,              0},
1706         {"full",        FULL,           0,              0},
1707         {"get_priority", GET_P,         0,              0},
1708         {"goto",        GOTO,           0,              0},
1709         {"hidden",      HIDDEN,         0,              ":hide:"},
1710         {"if",          IF,             0,              0},
1711         {"in",          IN,             0,              0},
1712         {"init",        INIT,           0,              ":init:"},
1713         {"inline",      INLINE,         0,              0},
1714         {"int",         TYPE,           INT,            0},
1715         {"len",         LEN,            0,              0},
1716         {"local",       ISLOCAL,        0,              ":local:"},
1717         {"ltl",         LTL,            0,              ":ltl:"},
1718         {"mtype",       TYPE,           MTYPE,          0},
1719         {"nempty",      NEMPTY,         0,              0},
1720         {"never",       CLAIM,          0,              ":never:"},
1721         {"nfull",       NFULL,          0,              0},
1722         {"notrace",     TRACE,          0,              ":notrace:"},
1723         {"np_",         NONPROGRESS,    0,              0},
1724         {"od",          OD,             0,              0},
1725         {"of",          OF,             0,              0},
1726         {"pc_value",    PC_VAL,         0,              0},
1727         {"pid",         TYPE,           BYTE,           0},
1728         {"printf",      PRINT,          0,              0},
1729         {"printm",      PRINTM,         0,              0},
1730         {"priority",    PRIORITY,       0,              0},
1731         {"proctype",    PROCTYPE,       0,              0},
1732         {"provided",    PROVIDED,       0,              0},
1733         {"return",      RETURN,         0,              0},
1734         {"run",         RUN,            0,              0},
1735         {"d_step",      D_STEP,         0,              0},
1736         {"select",      SELECT,         0,              0},
1737         {"set_priority", SET_P,         0,              0},
1738         {"short",       TYPE,           SHORT,          0},
1739         {"skip",        CONST,          1,              0},
1740         {"timeout",     TIMEOUT,        0,              0},
1741         {"trace",       TRACE,          0,              ":trace:"},
1742         {"true",        CONST,          1,              0},
1743         {"show",        SHOW,           0,              ":show:"},
1744         {"typedef",     TYPEDEF,        0,              0},
1745         {"unless",      UNLESS,         0,              0},
1746         {"unsigned",    TYPE,           UNSIGNED,       0},
1747         {"xr",          XU,             XR,             0},
1748         {"xs",          XU,             XS,             0},
1749         {0,             0,              0,              0},
1750 };
1751
1752 static int
1753 check_name(char *s)
1754 {       int i;
1755
1756         yylval = nn(ZN, 0, ZN, ZN);
1757
1758         if (ltl_mode)
1759         {       for (i = 0; LTL_syms[i].s; i++)
1760                 {       if (strcmp(s, LTL_syms[i].s) == 0)
1761                         {       return LTL_syms[i].tok;
1762         }       }       }
1763
1764         for (i = 0; Names[i].s; i++)
1765         {       if (strcmp(s, Names[i].s) == 0)
1766                 {       yylval->val = Names[i].val;
1767                         if (Names[i].sym)
1768                                 yylval->sym = lookup(Names[i].sym);
1769                         if (Names[i].tok == IN && !in_for)
1770                         {       continue;
1771                         }
1772                         return Names[i].tok;
1773         }       }
1774
1775         if ((yylval->val = ismtype(s)) != 0)
1776         {       yylval->ismtyp = 1;
1777                 return CONST;
1778         }
1779
1780         if (strcmp(s, "_last") == 0)
1781                 has_last++;
1782
1783         if (strcmp(s, "_priority") == 0)
1784                 has_priority++;
1785
1786         if (Inlining >= 0 && !ReDiRect)
1787         {       Lextok *tt, *t = Inline_stub[Inlining]->params;
1788
1789                 for (i = 0; t; t = t->rgt, i++)                         /* formal pars */
1790                  if (!strcmp(s, t->lft->sym->name)                      /* varname matches formal */
1791                  &&   strcmp(s, Inline_stub[Inlining]->anms[i]) != 0)   /* actual pars */
1792                  {
1793 #if 0
1794                         if (verbose&32)
1795                         printf("\tline %d, replace %s in call of '%s' with %s\n",
1796                                 lineno, s,
1797                                 Inline_stub[Inlining]->nm->name,
1798                                 Inline_stub[Inlining]->anms[i]);
1799 #endif
1800                         for (tt = Inline_stub[Inlining]->params; tt; tt = tt->rgt)
1801                                 if (!strcmp(Inline_stub[Inlining]->anms[i],
1802                                         tt->lft->sym->name))
1803                                 {       /* would be cyclic if not caught */
1804                                         printf("spin: %s:%d replacement value: %s\n",
1805                                                 oFname->name?oFname->name:"--", lineno, tt->lft->sym->name);
1806                                         fatal("formal par of %s contains replacement value",
1807                                                 Inline_stub[Inlining]->nm->name);
1808                                         yylval->ntyp = tt->lft->ntyp;
1809                                         yylval->sym = lookup(tt->lft->sym->name);
1810                                         return NAME;
1811                                 }
1812
1813                         /* check for occurrence of param as field of struct */
1814                         { char *ptr = Inline_stub[Inlining]->anms[i];
1815                                 while ((ptr = strstr(ptr, s)) != NULL)
1816                                 {       if (*(ptr-1) == '.'
1817                                         ||  *(ptr+strlen(s)) == '.')
1818                                         {       fatal("formal par of %s used in structure name",
1819                                                 Inline_stub[Inlining]->nm->name);
1820                                         }
1821                                         ptr++;
1822                         }       }
1823                         ReDiRect = Inline_stub[Inlining]->anms[i];
1824                         return 0;
1825         }        }
1826
1827         yylval->sym = lookup(s);        /* symbol table */
1828         if (isutype(s))
1829                 return UNAME;
1830         if (isproctype(s))
1831                 return PNAME;
1832         if (iseqname(s))
1833                 return INAME;
1834
1835         return NAME;
1836 }
1837
1838 int
1839 yylex(void)
1840 {       static int last = 0;
1841         static int hold = 0;
1842         int c;
1843         /*
1844          * repair two common syntax mistakes with
1845          * semi-colons before or after a '}'
1846          */
1847         if (hold)
1848         {       c = hold;
1849                 hold = 0;
1850                 last_token = c;
1851         } else
1852         {       c = lex();
1853                 if (last == ELSE
1854                 &&  c != SEMI
1855                 &&  c != ARROW
1856                 &&  c != FI)
1857                 {       hold = c;
1858                         last = 0;
1859                         last_token = SEMI;
1860                         return SEMI;
1861                 }
1862                 if (last == '}'
1863                 &&  c != PROCTYPE
1864                 &&  c != INIT
1865                 &&  c != CLAIM
1866                 &&  c != SEP
1867                 &&  c != FI
1868                 &&  c != OD
1869                 &&  c != '}'
1870                 &&  c != UNLESS
1871                 &&  c != SEMI
1872                 &&  c != ARROW
1873                 &&  c != EOF)
1874                 {       hold = c;
1875                         last = 0;
1876                         last_token = SEMI;
1877                         return SEMI;    /* insert ';' */
1878                 }
1879                 if (c == SEMI || c == ARROW)
1880                 {       /* if context, we're not in a typedef
1881                          * because they're global.
1882                          * if owner, we're at the end of a ref
1883                          * to a struct field -- prevent that the
1884                          * lookahead is interpreted as a field of
1885                          * the same struct...
1886                          */
1887                         if (context) owner = ZS;
1888                         hold = lex();   /* look ahead */
1889                         if (hold == '}'
1890                         ||  hold == ARROW
1891                         ||  hold == SEMI)
1892                         {       c = hold; /* omit ';' */
1893                                 hold = 0;
1894                         }
1895                 }
1896         }
1897         last = c;
1898
1899         if (IArgs)
1900         {       static int IArg_nst = 0;
1901
1902                 if (strcmp(yytext, ",") == 0)
1903                 {       IArg_cont[++IArgno][0] = '\0';
1904                 } else if (strcmp(yytext, "(") == 0)
1905                 {       if (IArg_nst++ == 0)
1906                         {       IArgno = 0;
1907                                 IArg_cont[0][0] = '\0';
1908                         } else
1909                         {       assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont));
1910                                 strcat(IArg_cont[IArgno], yytext);
1911                         }
1912                 } else if (strcmp(yytext, ")") == 0)
1913                 {       if (--IArg_nst > 0)
1914                         {       assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont));
1915                                 strcat(IArg_cont[IArgno], yytext);
1916                         }
1917                 } else if (c == CONST && yytext[0] == '\'')
1918                 {       sprintf(yytext, "'%c'", yylval->val);
1919                         assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont));
1920                         strcat(IArg_cont[IArgno], yytext);
1921                 } else if (c == CONST)
1922                 {       sprintf(yytext, "%d", yylval->val);
1923                         assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont));
1924                         strcat(IArg_cont[IArgno], yytext);
1925                 } else
1926                 {
1927                         switch (c) {
1928                         case ARROW:     strcpy(yytext, "->"); break; /* NEW */
1929                         case SEP:       strcpy(yytext, "::"); break;
1930                         case SEMI:      strcpy(yytext, ";"); break;
1931                         case DECR:      strcpy(yytext, "--"); break;
1932                         case INCR:      strcpy(yytext, "++"); break;
1933                         case LSHIFT:    strcpy(yytext, "<<"); break;
1934                         case RSHIFT:    strcpy(yytext, ">>"); break;
1935                         case LE:        strcpy(yytext, "<="); break;
1936                         case LT:        strcpy(yytext, "<"); break;
1937                         case GE:        strcpy(yytext, ">="); break;
1938                         case GT:        strcpy(yytext, ">"); break;
1939                         case EQ:        strcpy(yytext, "=="); break;
1940                         case ASGN:      strcpy(yytext, "="); break;
1941                         case NE:        strcpy(yytext, "!="); break;
1942                         case R_RCV:     strcpy(yytext, "??"); break;
1943                         case RCV:       strcpy(yytext, "?"); break;
1944                         case O_SND:     strcpy(yytext, "!!"); break;
1945                         case SND:       strcpy(yytext, "!"); break;
1946                         case AND:       strcpy(yytext, "&&"); break;
1947                         case OR:        strcpy(yytext, "||"); break;
1948                         }
1949                         assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont));
1950                         strcat(IArg_cont[IArgno], yytext);
1951                 }
1952         }
1953         return c;
1954 }