1 /***** spin: spinlex.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 "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 char **anms; /* literal text for actual pars */
25 char *prec; /* precondition for c_code or c_expr */
26 int uiid; /* unique inline id */
27 int dln, cln; /* def and call linenr */
28 Symbol *dfn, *cfn; /* def and call filename */
29 struct IType *nxt; /* linked list */
30 } IType;
31
32 typedef struct C_Added {
33 Symbol *s;
34 Symbol *t;
35 Symbol *ival;
36 struct C_Added *nxt;
37 } C_Added;
38
39 extern RunList *X;
40 extern ProcList *rdy;
41 extern Symbol *Fname, *oFname;
42 extern Symbol *context, *owner;
43 extern YYSTYPE yylval;
44 extern short has_last, has_code;
45 extern int verbose, IArgs, hastrack, separate, ltl_mode;
46
47 short has_stack = 0;
48 int lineno = 1;
49 int scope_seq[128], scope_level = 0;
50 char CurScope[MAXSCOPESZ];
51 char yytext[2048];
52 FILE *yyin, *yyout;
53
54 static C_Added *c_added, *c_tracked;
55 static IType *Inline_stub[MAXINL];
56 static char *ReDiRect;
57 static char *Inliner[MAXINL], IArg_cont[MAXPAR][MAXLEN];
58 static unsigned char in_comment=0;
59 static int IArgno = 0, Inlining = -1;
60 static int check_name(char *);
61
62 #if 1
63 #define Token(y) { if (in_comment) goto again; \
64 yylval = nn(ZN,0,ZN,ZN); return y; }
65
66 #define ValToken(x, y) { if (in_comment) goto again; \
67 yylval = nn(ZN,0,ZN,ZN); yylval->val = x; return y; }
68
69 #define SymToken(x, y) { if (in_comment) goto again; \
70 yylval = nn(ZN,0,ZN,ZN); yylval->sym = x; return y; }
71 #else
72 #define Token(y) { yylval = nn(ZN,0,ZN,ZN); \
73 if (!in_comment) return y; else goto again; }
74
75 #define ValToken(x, y) { yylval = nn(ZN,0,ZN,ZN); yylval->val = x; \
76 if (!in_comment) return y; else goto again; }
77
78 #define SymToken(x, y) { yylval = nn(ZN,0,ZN,ZN); yylval->sym = x; \
79 if (!in_comment) return y; else goto again; }
80 #endif
81
82 static int getinline(void);
83 static void uninline(void);
84
85 #if 1
86 #define Getchar() ((Inlining<0)?getc(yyin):getinline())
87 #define Ungetch(c) {if (Inlining<0) ungetc(c,yyin); else uninline();}
88
89 #else
90
91 static int
Getchar(void)92 Getchar(void)
93 { int c;
94
95 if (Inlining<0)
96 c = getc(yyin);
97 else
98 c = getinline();
99 if (0)
100 { printf("<%c:%d>[%d] ", c, c, Inlining);
101 } else
102 { printf("%c", c);
103 }
104 return c;
105 }
106
107 static void
Ungetch(int c)108 Ungetch(int c)
109 {
110 if (Inlining<0)
111 ungetc(c,yyin);
112 else
113 uninline();
114 if (0)
115 { printf("<bs>");
116 }
117 }
118 #endif
119
120 static int
notdollar(int c)121 notdollar(int c)
122 { return (c != '$' && c != '\n');
123 }
124
125 static int
notquote(int c)126 notquote(int c)
127 { return (c != '\"' && c != '\n');
128 }
129
130 int
isalnum_(int c)131 isalnum_(int c)
132 { return (isalnum(c) || c == '_');
133 }
134
135 static int
isalpha_(int c)136 isalpha_(int c)
137 { return isalpha(c); /* could be macro */
138 }
139
140 static int
isdigit_(int c)141 isdigit_(int c)
142 { return isdigit(c); /* could be macro */
143 }
144
145 static void
getword(int first,int (* tst)(int))146 getword(int first, int (*tst)(int))
147 { int i=0, c;
148
149 yytext[i++]= (char) first;
150 while (tst(c = Getchar()))
151 { yytext[i++] = (char) c;
152 if (c == '\\')
153 { c = Getchar();
154 yytext[i++] = (char) c; /* no tst */
155 } }
156 yytext[i] = '\0';
157 Ungetch(c);
158 }
159
160 static int
follow(int tok,int ifyes,int ifno)161 follow(int tok, int ifyes, int ifno)
162 { int c;
163
164 if ((c = Getchar()) == tok)
165 return ifyes;
166 Ungetch(c);
167
168 return ifno;
169 }
170
171 static IType *seqnames;
172
173 static void
def_inline(Symbol * s,int ln,char * ptr,char * prc,Lextok * nms)174 def_inline(Symbol *s, int ln, char *ptr, char *prc, Lextok *nms)
175 { IType *tmp;
176 int cnt = 0;
177 char *nw = (char *) emalloc(strlen(ptr)+1);
178 strcpy(nw, ptr);
179
180 for (tmp = seqnames; tmp; cnt++, tmp = tmp->nxt)
181 if (!strcmp(s->name, tmp->nm->name))
182 { non_fatal("procedure name %s redefined",
183 tmp->nm->name);
184 tmp->cn = (Lextok *) nw;
185 tmp->params = nms;
186 tmp->dln = ln;
187 tmp->dfn = Fname;
188 return;
189 }
190 tmp = (IType *) emalloc(sizeof(IType));
191 tmp->nm = s;
192 tmp->cn = (Lextok *) nw;
193 tmp->params = nms;
194 if (strlen(prc) > 0)
195 { tmp->prec = (char *) emalloc(strlen(prc)+1);
196 strcpy(tmp->prec, prc);
197 }
198 tmp->dln = ln;
199 tmp->dfn = Fname;
200 tmp->uiid = cnt+1; /* so that 0 means: not an inline */
201 tmp->nxt = seqnames;
202 seqnames = tmp;
203 }
204
205 void
gencodetable(FILE * fd)206 gencodetable(FILE *fd)
207 { IType *tmp;
208 char *q;
209 int cnt;
210
211 if (separate == 2) return;
212
213 fprintf(fd, "struct {\n");
214 fprintf(fd, " char *c; char *t;\n");
215 fprintf(fd, "} code_lookup[] = {\n");
216
217 if (has_code)
218 for (tmp = seqnames; tmp; tmp = tmp->nxt)
219 if (tmp->nm->type == CODE_FRAG
220 || tmp->nm->type == CODE_DECL)
221 { fprintf(fd, "\t{ \"%s\", ",
222 tmp->nm->name);
223 q = (char *) tmp->cn;
224
225 while (*q == '\n' || *q == '\r' || *q == '\\')
226 q++;
227
228 fprintf(fd, "\"");
229 cnt = 0;
230 while (*q && cnt < 1024) /* pangen1.h allows 2048 */
231 { switch (*q) {
232 case '"':
233 fprintf(fd, "\\\"");
234 break;
235 case '%':
236 fprintf(fd, "%%");
237 break;
238 case '\n':
239 fprintf(fd, "\\n");
240 break;
241 default:
242 putc(*q, fd);
243 break;
244 }
245 q++; cnt++;
246 }
247 if (*q) fprintf(fd, "...");
248 fprintf(fd, "\"");
249 fprintf(fd, " },\n");
250 }
251
252 fprintf(fd, " { (char *) 0, \"\" }\n");
253 fprintf(fd, "};\n");
254 }
255
256 static int
iseqname(char * t)257 iseqname(char *t)
258 { IType *tmp;
259
260 for (tmp = seqnames; tmp; tmp = tmp->nxt)
261 { if (!strcmp(t, tmp->nm->name))
262 return 1;
263 }
264 return 0;
265 }
266
267 static int
getinline(void)268 getinline(void)
269 { int c;
270
271 if (ReDiRect)
272 { c = *ReDiRect++;
273 if (c == '\0')
274 { ReDiRect = (char *) 0;
275 c = *Inliner[Inlining]++;
276 }
277 } else
278 c = *Inliner[Inlining]++;
279
280 if (c == '\0')
281 { lineno = Inline_stub[Inlining]->cln;
282 Fname = Inline_stub[Inlining]->cfn;
283 Inlining--;
284 #if 0
285 if (verbose&32)
286 printf("spin: %s:%d, done inlining %s\n",
287 Fname, lineno, Inline_stub[Inlining+1]->nm->name);
288 #endif
289 return Getchar();
290 }
291 return c;
292 }
293
294 static void
uninline(void)295 uninline(void)
296 {
297 if (ReDiRect)
298 ReDiRect--;
299 else
300 Inliner[Inlining]--;
301 }
302
303 int
is_inline(void)304 is_inline(void)
305 {
306 if (Inlining < 0)
307 return 0; /* i.e., not an inline */
308 if (Inline_stub[Inlining] == NULL)
309 fatal("unexpected, inline_stub not set", 0);
310 return Inline_stub[Inlining]->uiid;
311 }
312
313 IType *
find_inline(char * s)314 find_inline(char *s)
315 { IType *tmp;
316
317 for (tmp = seqnames; tmp; tmp = tmp->nxt)
318 if (!strcmp(s, tmp->nm->name))
319 break;
320 if (!tmp)
321 fatal("cannot happen, missing inline def %s", s);
322
323 return tmp;
324 }
325
326 void
c_state(Symbol * s,Symbol * t,Symbol * ival)327 c_state(Symbol *s, Symbol *t, Symbol *ival) /* name, scope, ival */
328 { C_Added *r;
329
330 r = (C_Added *) emalloc(sizeof(C_Added));
331 r->s = s; /* pointer to a data object */
332 r->t = t; /* size of object, or "global", or "local proctype_name" */
333 r->ival = ival;
334 r->nxt = c_added;
335 c_added = r;
336 }
337
338 void
c_track(Symbol * s,Symbol * t,Symbol * stackonly)339 c_track(Symbol *s, Symbol *t, Symbol *stackonly) /* name, size */
340 { C_Added *r;
341
342 r = (C_Added *) emalloc(sizeof(C_Added));
343 r->s = s;
344 r->t = t;
345 r->ival = stackonly; /* abuse of name */
346 r->nxt = c_tracked;
347 c_tracked = r;
348
349 if (stackonly != ZS)
350 { if (strcmp(stackonly->name, "\"Matched\"") == 0)
351 r->ival = ZS; /* the default */
352 else if (strcmp(stackonly->name, "\"UnMatched\"") != 0
353 && strcmp(stackonly->name, "\"unMatched\"") != 0
354 && strcmp(stackonly->name, "\"StackOnly\"") != 0)
355 non_fatal("expecting '[Un]Matched', saw %s", stackonly->name);
356 else
357 has_stack = 1; /* unmatched stack */
358 }
359 }
360
361 char *
jump_etc(char * op)362 jump_etc(char *op)
363 { char *p = op;
364
365 /* kludgy - try to get the type separated from the name */
366
367 while (*p == ' ' || *p == '\t')
368 p++; /* initial white space */
369 while (*p != ' ' && *p != '\t')
370 p++; /* type name */
371 while (*p == ' ' || *p == '\t')
372 p++; /* white space */
373 while (*p == '*')
374 p++; /* decorations */
375 while (*p == ' ' || *p == '\t')
376 p++; /* white space */
377
378 if (*p == '\0')
379 fatal("c_state format (%s)", op);
380
381 if (strchr(p, '[')
382 && !strchr(p, '{'))
383 { non_fatal("array initialization error, c_state (%s)", p);
384 return (char *) 0;
385 }
386
387 return p;
388 }
389
390 void
c_add_globinit(FILE * fd)391 c_add_globinit(FILE *fd)
392 { C_Added *r;
393 char *p, *q;
394
395 fprintf(fd, "void\nglobinit(void)\n{\n");
396 for (r = c_added; r; r = r->nxt)
397 { if (r->ival == ZS)
398 continue;
399
400 if (strncmp(r->t->name, " Global ", strlen(" Global ")) == 0)
401 { for (q = r->ival->name; *q; q++)
402 { if (*q == '\"')
403 *q = ' ';
404 if (*q == '\\')
405 *q++ = ' '; /* skip over the next */
406 }
407 p = jump_etc(r->s->name); /* e.g., "int **q" */
408 if (p)
409 fprintf(fd, " now.%s = %s;\n", p, r->ival->name);
410
411 } else
412 if (strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) == 0)
413 { for (q = r->ival->name; *q; q++)
414 { if (*q == '\"')
415 *q = ' ';
416 if (*q == '\\')
417 *q++ = ' '; /* skip over the next */
418 }
419 p = jump_etc(r->s->name); /* e.g., "int **q" */
420 if (p)
421 fprintf(fd, " %s = %s;\n", p, r->ival->name); /* no now. prefix */
422
423 } }
424 fprintf(fd, "}\n");
425 }
426
427 void
c_add_locinit(FILE * fd,int tpnr,char * pnm)428 c_add_locinit(FILE *fd, int tpnr, char *pnm)
429 { C_Added *r;
430 char *p, *q, *s;
431 int frst = 1;
432
433 fprintf(fd, "void\nlocinit%d(int h)\n{\n", tpnr);
434 for (r = c_added; r; r = r->nxt)
435 if (r->ival != ZS
436 && strncmp(r->t->name, " Local", strlen(" Local")) == 0)
437 { for (q = r->ival->name; *q; q++)
438 if (*q == '\"')
439 *q = ' ';
440
441 p = jump_etc(r->s->name); /* e.g., "int **q" */
442
443 q = r->t->name + strlen(" Local");
444 while (*q == ' ' || *q == '\t')
445 q++; /* process name */
446
447 s = (char *) emalloc(strlen(q)+1);
448 strcpy(s, q);
449
450 q = &s[strlen(s)-1];
451 while (*q == ' ' || *q == '\t')
452 *q-- = '\0';
453
454 if (strcmp(pnm, s) != 0)
455 continue;
456
457 if (frst)
458 { fprintf(fd, "\tuchar *this = pptr(h);\n");
459 frst = 0;
460 }
461
462 if (p)
463 fprintf(fd, " ((P%d *)this)->%s = %s;\n",
464 tpnr, p, r->ival->name);
465
466 }
467 fprintf(fd, "}\n");
468 }
469
470 /* tracking:
471 1. for non-global and non-local c_state decls: add up all the sizes in c_added
472 2. add a global char array of that size into now
473 3. generate a routine that memcpy's the required values into that array
474 4. generate a call to that routine
475 */
476
477 void
c_preview(void)478 c_preview(void)
479 { C_Added *r;
480
481 hastrack = 0;
482 if (c_tracked)
483 hastrack = 1;
484 else
485 for (r = c_added; r; r = r->nxt)
486 if (strncmp(r->t->name, " Global ", strlen(" Global ")) != 0
487 && strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) != 0
488 && strncmp(r->t->name, " Local", strlen(" Local")) != 0)
489 { hastrack = 1; /* c_state variant now obsolete */
490 break;
491 }
492 }
493
494 int
c_add_sv(FILE * fd)495 c_add_sv(FILE *fd) /* 1+2 -- called in pangen1.c */
496 { C_Added *r;
497 int cnt = 0;
498
499 if (!c_added && !c_tracked) return 0;
500
501 for (r = c_added; r; r = r->nxt) /* pickup global decls */
502 if (strncmp(r->t->name, " Global ", strlen(" Global ")) == 0)
503 fprintf(fd, " %s;\n", r->s->name);
504
505 for (r = c_added; r; r = r->nxt)
506 if (strncmp(r->t->name, " Global ", strlen(" Global ")) != 0
507 && strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) != 0
508 && strncmp(r->t->name, " Local", strlen(" Local")) != 0)
509 { cnt++; /* obsolete use */
510 }
511
512 for (r = c_tracked; r; r = r->nxt)
513 cnt++; /* preferred use */
514
515 if (cnt == 0) return 0;
516
517 cnt = 0;
518 fprintf(fd, " uchar c_state[");
519 for (r = c_added; r; r = r->nxt)
520 if (strncmp(r->t->name, " Global ", strlen(" Global ")) != 0
521 && strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) != 0
522 && strncmp(r->t->name, " Local", strlen(" Local")) != 0)
523 { fprintf(fd, "%ssizeof(%s)",
524 (cnt==0)?"":"+", r->t->name);
525 cnt++;
526 }
527
528 for (r = c_tracked; r; r = r->nxt)
529 { if (r->ival != ZS) continue;
530
531 fprintf(fd, "%s%s",
532 (cnt==0)?"":"+", r->t->name);
533 cnt++;
534 }
535
536 if (cnt == 0) fprintf(fd, "4"); /* now redundant */
537 fprintf(fd, "];\n");
538 return 1;
539 }
540
541 void
c_stack_size(FILE * fd)542 c_stack_size(FILE *fd)
543 { C_Added *r;
544 int cnt = 0;
545
546 for (r = c_tracked; r; r = r->nxt)
547 if (r->ival != ZS)
548 { fprintf(fd, "%s%s",
549 (cnt==0)?"":"+", r->t->name);
550 cnt++;
551 }
552 if (cnt == 0)
553 { fprintf(fd, "WS");
554 }
555 }
556
557 void
c_add_stack(FILE * fd)558 c_add_stack(FILE *fd)
559 { C_Added *r;
560 int cnt = 0;
561
562 if ((!c_added && !c_tracked) || !has_stack)
563 { return;
564 }
565
566 for (r = c_tracked; r; r = r->nxt)
567 if (r->ival != ZS)
568 { cnt++;
569 }
570
571 if (cnt > 0)
572 { fprintf(fd, " uchar c_stack[StackSize];\n");
573 }
574 }
575
576 void
c_add_hidden(FILE * fd)577 c_add_hidden(FILE *fd)
578 { C_Added *r;
579
580 for (r = c_added; r; r = r->nxt) /* pickup hidden decls */
581 if (strncmp(r->t->name, "\"Hidden\"", strlen("\"Hidden\"")) == 0)
582 { r->s->name[strlen(r->s->name)-1] = ' ';
583 fprintf(fd, "%s; /* Hidden */\n", &r->s->name[1]);
584 r->s->name[strlen(r->s->name)-1] = '"';
585 }
586 /* called before c_add_def - quotes are still there */
587 }
588
589 void
c_add_loc(FILE * fd,char * s)590 c_add_loc(FILE *fd, char *s) /* state vector entries for proctype s */
591 { C_Added *r;
592 static char buf[1024];
593 char *p;
594
595 if (!c_added) return;
596
597 strcpy(buf, s);
598 strcat(buf, " ");
599 for (r = c_added; r; r = r->nxt) /* pickup local decls */
600 if (strncmp(r->t->name, " Local", strlen(" Local")) == 0)
601 { p = r->t->name + strlen(" Local");
602 while (*p == ' ' || *p == '\t')
603 p++;
604 if (strcmp(p, buf) == 0)
605 fprintf(fd, " %s;\n", r->s->name);
606 }
607 }
608 void
c_add_def(FILE * fd)609 c_add_def(FILE *fd) /* 3 - called in plunk_c_fcts() */
610 { C_Added *r;
611
612 fprintf(fd, "#if defined(C_States) && defined(HAS_TRACK)\n");
613 for (r = c_added; r; r = r->nxt)
614 { r->s->name[strlen(r->s->name)-1] = ' ';
615 r->s->name[0] = ' '; /* remove the "s */
616
617 r->t->name[strlen(r->t->name)-1] = ' ';
618 r->t->name[0] = ' ';
619
620 if (strncmp(r->t->name, " Global ", strlen(" Global ")) == 0
621 || strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) == 0
622 || strncmp(r->t->name, " Local", strlen(" Local")) == 0)
623 continue;
624
625 if (strchr(r->s->name, '&'))
626 fatal("dereferencing state object: %s", r->s->name);
627
628 fprintf(fd, "extern %s %s;\n", r->t->name, r->s->name);
629 }
630 for (r = c_tracked; r; r = r->nxt)
631 { r->s->name[strlen(r->s->name)-1] = ' ';
632 r->s->name[0] = ' '; /* remove " */
633
634 r->t->name[strlen(r->t->name)-1] = ' ';
635 r->t->name[0] = ' ';
636 }
637
638 if (separate == 2)
639 { fprintf(fd, "#endif\n");
640 return;
641 }
642
643 if (has_stack)
644 { fprintf(fd, "int cpu_printf(const char *, ...);\n");
645 fprintf(fd, "void\nc_stack(uchar *p_t_r)\n{\n");
646 fprintf(fd, "#ifdef VERBOSE\n");
647 fprintf(fd, " cpu_printf(\"c_stack %%u\\n\", p_t_r);\n");
648 fprintf(fd, "#endif\n");
649 for (r = c_tracked; r; r = r->nxt)
650 { if (r->ival == ZS) continue;
651
652 fprintf(fd, "\tif(%s)\n", r->s->name);
653 fprintf(fd, "\t\tmemcpy(p_t_r, %s, %s);\n",
654 r->s->name, r->t->name);
655 fprintf(fd, "\telse\n");
656 fprintf(fd, "\t\tmemset(p_t_r, 0, %s);\n",
657 r->t->name);
658 fprintf(fd, "\tp_t_r += %s;\n", r->t->name);
659 }
660 fprintf(fd, "}\n\n");
661 }
662
663 fprintf(fd, "void\nc_update(uchar *p_t_r)\n{\n");
664 fprintf(fd, "#ifdef VERBOSE\n");
665 fprintf(fd, " printf(\"c_update %%u\\n\", p_t_r);\n");
666 fprintf(fd, "#endif\n");
667 for (r = c_added; r; r = r->nxt)
668 { if (strncmp(r->t->name, " Global ", strlen(" Global ")) == 0
669 || strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) == 0
670 || strncmp(r->t->name, " Local", strlen(" Local")) == 0)
671 continue;
672
673 fprintf(fd, "\tmemcpy(p_t_r, &%s, sizeof(%s));\n",
674 r->s->name, r->t->name);
675 fprintf(fd, "\tp_t_r += sizeof(%s);\n", r->t->name);
676 }
677
678 for (r = c_tracked; r; r = r->nxt)
679 { if (r->ival) continue;
680
681 fprintf(fd, "\tif(%s)\n", r->s->name);
682 fprintf(fd, "\t\tmemcpy(p_t_r, %s, %s);\n",
683 r->s->name, r->t->name);
684 fprintf(fd, "\telse\n");
685 fprintf(fd, "\t\tmemset(p_t_r, 0, %s);\n",
686 r->t->name);
687 fprintf(fd, "\tp_t_r += %s;\n", r->t->name);
688 }
689
690 fprintf(fd, "}\n");
691
692 if (has_stack)
693 { fprintf(fd, "void\nc_unstack(uchar *p_t_r)\n{\n");
694 fprintf(fd, "#ifdef VERBOSE\n");
695 fprintf(fd, " cpu_printf(\"c_unstack %%u\\n\", p_t_r);\n");
696 fprintf(fd, "#endif\n");
697 for (r = c_tracked; r; r = r->nxt)
698 { if (r->ival == ZS) continue;
699
700 fprintf(fd, "\tif(%s)\n", r->s->name);
701 fprintf(fd, "\t\tmemcpy(%s, p_t_r, %s);\n",
702 r->s->name, r->t->name);
703 fprintf(fd, "\tp_t_r += %s;\n", r->t->name);
704 }
705 fprintf(fd, "}\n");
706 }
707
708 fprintf(fd, "void\nc_revert(uchar *p_t_r)\n{\n");
709 fprintf(fd, "#ifdef VERBOSE\n");
710 fprintf(fd, " printf(\"c_revert %%u\\n\", p_t_r);\n");
711 fprintf(fd, "#endif\n");
712 for (r = c_added; r; r = r->nxt)
713 { if (strncmp(r->t->name, " Global ", strlen(" Global ")) == 0
714 || strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) == 0
715 || strncmp(r->t->name, " Local", strlen(" Local")) == 0)
716 continue;
717
718 fprintf(fd, "\tmemcpy(&%s, p_t_r, sizeof(%s));\n",
719 r->s->name, r->t->name);
720 fprintf(fd, "\tp_t_r += sizeof(%s);\n", r->t->name);
721 }
722 for (r = c_tracked; r; r = r->nxt)
723 { if (r->ival != ZS) continue;
724
725 fprintf(fd, "\tif(%s)\n", r->s->name);
726 fprintf(fd, "\t\tmemcpy(%s, p_t_r, %s);\n",
727 r->s->name, r->t->name);
728 fprintf(fd, "\tp_t_r += %s;\n", r->t->name);
729 }
730
731 fprintf(fd, "}\n");
732 fprintf(fd, "#endif\n");
733 }
734
735 void
plunk_reverse(FILE * fd,IType * p,int matchthis)736 plunk_reverse(FILE *fd, IType *p, int matchthis)
737 { char *y, *z;
738
739 if (!p) return;
740 plunk_reverse(fd, p->nxt, matchthis);
741
742 if (!p->nm->context
743 && p->nm->type == matchthis)
744 { fprintf(fd, "\n/* start of %s */\n", p->nm->name);
745 z = (char *) p->cn;
746 while (*z == '\n' || *z == '\r' || *z == '\\')
747 z++;
748 /* e.g.: \#include "..." */
749
750 y = z;
751 while ((y = strstr(y, "\\#")) != NULL)
752 { *y = '\n'; y++;
753 }
754
755 fprintf(fd, "%s\n", z);
756 fprintf(fd, "\n/* end of %s */\n", p->nm->name);
757 }
758 }
759
760 void
plunk_c_decls(FILE * fd)761 plunk_c_decls(FILE *fd)
762 {
763 plunk_reverse(fd, seqnames, CODE_DECL);
764 }
765
766 void
plunk_c_fcts(FILE * fd)767 plunk_c_fcts(FILE *fd)
768 {
769 if (separate == 2 && hastrack)
770 { c_add_def(fd);
771 return;
772 }
773
774 c_add_hidden(fd);
775 plunk_reverse(fd, seqnames, CODE_FRAG);
776
777 if (c_added || c_tracked) /* enables calls to c_revert and c_update */
778 fprintf(fd, "#define C_States 1\n");
779 else
780 fprintf(fd, "#undef C_States\n");
781
782 if (hastrack)
783 c_add_def(fd);
784
785 c_add_globinit(fd);
786 do_locinits(fd);
787 }
788
789 static void
check_inline(IType * tmp)790 check_inline(IType *tmp)
791 { char buf[128];
792 ProcList *p;
793
794 if (!X) return;
795
796 for (p = rdy; p; p = p->nxt)
797 { if (strcmp(p->n->name, X->n->name) == 0)
798 continue;
799 sprintf(buf, "P%s->", p->n->name);
800 if (strstr((char *)tmp->cn, buf))
801 { printf("spin: in proctype %s, ref to object in proctype %s\n",
802 X->n->name, p->n->name);
803 fatal("invalid variable ref in '%s'", tmp->nm->name);
804 } }
805 }
806
807 void
plunk_expr(FILE * fd,char * s)808 plunk_expr(FILE *fd, char *s)
809 { IType *tmp;
810
811 tmp = find_inline(s);
812 check_inline(tmp);
813
814 fprintf(fd, "%s", (char *) tmp->cn);
815 }
816
817 void
preruse(FILE * fd,Lextok * n)818 preruse(FILE *fd, Lextok *n) /* check a condition for c_expr with preconditions */
819 { IType *tmp;
820
821 if (!n) return;
822 if (n->ntyp == C_EXPR)
823 { tmp = find_inline(n->sym->name);
824 if (tmp->prec)
825 { fprintf(fd, "if (!(%s)) { if (!readtrail) { depth++; ", tmp->prec);
826 fprintf(fd, "trpt++; trpt->pr = II; trpt->o_t = t;");
827 fprintf(fd, "trpt->st = tt; uerror(\"%s\"); continue; } ", tmp->prec);
828 fprintf(fd, "else { printf(\"pan: precondition false: %s\\n\"); ", tmp->prec);
829 fprintf(fd, "_m = 3; goto P999; } } \n\t\t");
830 }
831 } else
832 { preruse(fd, n->rgt);
833 preruse(fd, n->lft);
834 }
835 }
836
837 int
glob_inline(char * s)838 glob_inline(char *s)
839 { IType *tmp;
840 char *bdy;
841
842 tmp = find_inline(s);
843 bdy = (char *) tmp->cn;
844 return (strstr(bdy, "now.") /* global ref or */
845 || strchr(bdy, '(') > bdy); /* possible C-function call */
846 }
847
848 void
plunk_inline(FILE * fd,char * s,int how,int gencode)849 plunk_inline(FILE *fd, char *s, int how, int gencode) /* c_code with precondition */
850 { IType *tmp;
851
852 tmp = find_inline(s);
853 check_inline(tmp);
854
855 fprintf(fd, "{ ");
856 if (how && tmp->prec)
857 { fprintf(fd, "if (!(%s)) { if (!readtrail) {",
858 tmp->prec);
859 fprintf(fd, " uerror(\"%s\"); continue; ",
860 tmp->prec);
861 fprintf(fd, "} else { ");
862 fprintf(fd, "printf(\"pan: precondition false: %s\\n\"); _m = 3; goto P999; } } ",
863 tmp->prec);
864 }
865
866 if (!gencode) /* not in d_step */
867 { fprintf(fd, "\n\t\tsv_save();");
868 }
869
870 fprintf(fd, "%s", (char *) tmp->cn);
871 fprintf(fd, " }\n");
872 }
873
874 void
no_side_effects(char * s)875 no_side_effects(char *s)
876 { IType *tmp;
877 char *t;
878
879 /* could still defeat this check via hidden
880 * side effects in function calls,
881 * but this will catch at least some cases
882 */
883
884 tmp = find_inline(s);
885 t = (char *) tmp->cn;
886
887 if (strchr(t, ';')
888 || strstr(t, "++")
889 || strstr(t, "--"))
890 {
891 bad: lineno = tmp->dln;
892 Fname = tmp->dfn;
893 non_fatal("c_expr %s has side-effects", s);
894 return;
895 }
896 while ((t = strchr(t, '=')) != NULL)
897 { if (*(t-1) == '!'
898 || *(t-1) == '>'
899 || *(t-1) == '<')
900 { t++;
901 continue;
902 }
903 t++;
904 if (*t != '=')
905 goto bad;
906 t++;
907 }
908 }
909
910 void
pickup_inline(Symbol * t,Lextok * apars)911 pickup_inline(Symbol *t, Lextok *apars)
912 { IType *tmp; Lextok *p, *q; int j;
913
914 tmp = find_inline(t->name);
915
916 if (++Inlining >= MAXINL)
917 fatal("inlines nested too deeply", 0);
918 tmp->cln = lineno; /* remember calling point */
919 tmp->cfn = Fname; /* and filename */
920
921 for (p = apars, q = tmp->params, j = 0; p && q; p = p->rgt, q = q->rgt)
922 j++; /* count them */
923 if (p || q)
924 fatal("wrong nr of params on call of '%s'", t->name);
925
926 tmp->anms = (char **) emalloc(j * sizeof(char *));
927 for (p = apars, j = 0; p; p = p->rgt, j++)
928 { tmp->anms[j] = (char *) emalloc(strlen(IArg_cont[j])+1);
929 strcpy(tmp->anms[j], IArg_cont[j]);
930 }
931
932 lineno = tmp->dln; /* linenr of def */
933 Fname = tmp->dfn; /* filename of same */
934 Inliner[Inlining] = (char *)tmp->cn;
935 Inline_stub[Inlining] = tmp;
936 #if 0
937 if (verbose&32)
938 printf("spin: %s:%d, inlining '%s' (from %s:%d)\n",
939 tmp->cfn->name, tmp->cln, t->name, tmp->dfn->name, tmp->dln);
940 #endif
941 for (j = 0; j < Inlining; j++)
942 if (Inline_stub[j] == Inline_stub[Inlining])
943 fatal("cyclic inline attempt on: %s", t->name);
944 }
945
946 static void
do_directive(int first)947 do_directive(int first)
948 { int c = first; /* handles lines starting with pound */
949
950 getword(c, isalpha_);
951
952 if (strcmp(yytext, "#ident") == 0)
953 goto done;
954
955 if ((c = Getchar()) != ' ')
956 fatal("malformed preprocessor directive - # .", 0);
957
958 if (!isdigit_(c = Getchar()))
959 fatal("malformed preprocessor directive - # .lineno", 0);
960
961 getword(c, isdigit_);
962 lineno = atoi(yytext); /* pickup the line number */
963
964 if ((c = Getchar()) == '\n')
965 return; /* no filename */
966
967 if (c != ' ')
968 fatal("malformed preprocessor directive - .fname", 0);
969
970 if ((c = Getchar()) != '\"')
971 { printf("got %c, expected \" -- lineno %d\n", c, lineno);
972 fatal("malformed preprocessor directive - .fname (%s)", yytext);
973 }
974
975 getword(Getchar(), notquote); /* was getword(c, notquote); */
976 if (Getchar() != '\"')
977 fatal("malformed preprocessor directive - fname.", 0);
978
979 /* strcat(yytext, "\""); */
980 Fname = lookup(yytext);
981 done:
982 while (Getchar() != '\n')
983 ;
984 }
985
986 void
precondition(char * q)987 precondition(char *q)
988 { int c, nest = 1;
989
990 for (;;)
991 { c = Getchar();
992 *q++ = c;
993 switch (c) {
994 case '\n':
995 lineno++;
996 break;
997 case '[':
998 nest++;
999 break;
1000 case ']':
1001 if (--nest <= 0)
1002 { *--q = '\0';
1003 return;
1004 }
1005 break;
1006 }
1007 }
1008 fatal("cannot happen", (char *) 0); /* unreachable */
1009 }
1010
1011
1012 Symbol *
prep_inline(Symbol * s,Lextok * nms)1013 prep_inline(Symbol *s, Lextok *nms)
1014 { int c, nest = 1, dln, firstchar, cnr;
1015 char *p;
1016 Lextok *t;
1017 static char Buf1[SOMETHINGBIG], Buf2[RATHERSMALL];
1018 static int c_code = 1;
1019
1020 for (t = nms; t; t = t->rgt)
1021 if (t->lft)
1022 { if (t->lft->ntyp != NAME)
1023 fatal("bad param to inline %s", s?s->name:"--");
1024 t->lft->sym->hidden |= 32;
1025 }
1026
1027 if (!s) /* C_Code fragment */
1028 { s = (Symbol *) emalloc(sizeof(Symbol));
1029 s->name = (char *) emalloc(strlen("c_code")+26);
1030 sprintf(s->name, "c_code%d", c_code++);
1031 s->context = context;
1032 s->type = CODE_FRAG;
1033 } else
1034 s->type = PREDEF;
1035
1036 p = &Buf1[0];
1037 Buf2[0] = '\0';
1038 for (;;)
1039 { c = Getchar();
1040 switch (c) {
1041 case '[':
1042 if (s->type != CODE_FRAG)
1043 goto bad;
1044 precondition(&Buf2[0]); /* e.g., c_code [p] { r = p-r; } */
1045 continue;
1046 case '{':
1047 break;
1048 case '\n':
1049 lineno++;
1050 /* fall through */
1051 case ' ': case '\t': case '\f': case '\r':
1052 continue;
1053 default :
1054 printf("spin: saw char '%c'\n", c);
1055 bad: fatal("bad inline: %s", s->name);
1056 }
1057 break;
1058 }
1059 dln = lineno;
1060 if (s->type == CODE_FRAG)
1061 { if (verbose&32)
1062 sprintf(Buf1, "\t/* line %d %s */\n\t\t",
1063 lineno, Fname->name);
1064 else
1065 strcpy(Buf1, "");
1066 } else
1067 sprintf(Buf1, "\n#line %d \"%s\"\n{", lineno, Fname->name);
1068 p += strlen(Buf1);
1069 firstchar = 1;
1070
1071 cnr = 1; /* not zero */
1072 more:
1073 c = Getchar();
1074 *p++ = (char) c;
1075 if (p - Buf1 >= SOMETHINGBIG)
1076 fatal("inline text too long", 0);
1077 switch (c) {
1078 case '\n':
1079 lineno++;
1080 cnr = 0;
1081 break;
1082 case '{':
1083 cnr++;
1084 nest++;
1085 break;
1086 case '}':
1087 cnr++;
1088 if (--nest <= 0)
1089 { *p = '\0';
1090 if (s->type == CODE_FRAG)
1091 *--p = '\0'; /* remove trailing '}' */
1092 def_inline(s, dln, &Buf1[0], &Buf2[0], nms);
1093 if (firstchar)
1094 printf("%3d: %s, warning: empty inline definition (%s)\n",
1095 dln, Fname->name, s->name);
1096 return s; /* normal return */
1097 }
1098 break;
1099 case '#':
1100 if (cnr == 0)
1101 { p--;
1102 do_directive(c); /* reads to newline */
1103 } else
1104 { firstchar = 0;
1105 cnr++;
1106 }
1107 break;
1108 case '\t':
1109 case ' ':
1110 case '\f':
1111 cnr++;
1112 break;
1113 default:
1114 firstchar = 0;
1115 cnr++;
1116 break;
1117 }
1118 goto more;
1119 }
1120
1121 static void
set_cur_scope(void)1122 set_cur_scope(void)
1123 { int i;
1124 char tmpbuf[256];
1125
1126 strcpy(CurScope, "_");
1127
1128 if (context)
1129 for (i = 0; i < scope_level; i++)
1130 { sprintf(tmpbuf, "%d_", scope_seq[i]);
1131 strcat(CurScope, tmpbuf);
1132 }
1133 }
1134
1135 static int
lex(void)1136 lex(void)
1137 { int c;
1138
1139 again:
1140 c = Getchar();
1141 yytext[0] = (char) c;
1142 yytext[1] = '\0';
1143 switch (c) {
1144 case EOF:
1145 return c;
1146 case '\n': /* newline */
1147 lineno++;
1148 case '\r': /* carriage return */
1149 goto again;
1150
1151 case ' ': case '\t': case '\f': /* white space */
1152 goto again;
1153
1154 case '#': /* preprocessor directive */
1155 if (in_comment) goto again;
1156 do_directive(c);
1157 goto again;
1158
1159 case '\"':
1160 getword(c, notquote);
1161 if (Getchar() != '\"')
1162 fatal("string not terminated", yytext);
1163 strcat(yytext, "\"");
1164 SymToken(lookup(yytext), STRING)
1165
1166 case '$':
1167 getword('\"', notdollar);
1168 if (Getchar() != '$')
1169 fatal("ltl definition not terminated", yytext);
1170 strcat(yytext, "\"");
1171 SymToken(lookup(yytext), STRING)
1172
1173 case '\'': /* new 3.0.9 */
1174 c = Getchar();
1175 if (c == '\\')
1176 { c = Getchar();
1177 if (c == 'n') c = '\n';
1178 else if (c == 'r') c = '\r';
1179 else if (c == 't') c = '\t';
1180 else if (c == 'f') c = '\f';
1181 }
1182 if (Getchar() != '\'' && !in_comment)
1183 fatal("character quote missing: %s", yytext);
1184 ValToken(c, CONST)
1185
1186 default:
1187 break;
1188 }
1189
1190 if (isdigit_(c))
1191 { getword(c, isdigit_);
1192 ValToken(atoi(yytext), CONST)
1193 }
1194
1195 if (isalpha_(c) || c == '_')
1196 { getword(c, isalnum_);
1197 if (!in_comment)
1198 { c = check_name(yytext);
1199 if (c) return c;
1200 /* else fall through */
1201 }
1202 goto again;
1203 }
1204
1205 if (ltl_mode)
1206 { switch (c) {
1207 case '-': c = follow('>', IMPLIES, '-'); break;
1208 case '[': c = follow(']', ALWAYS, '['); break;
1209 case '<': c = follow('>', EVENTUALLY, '<');
1210 if (c == '<')
1211 { c = Getchar();
1212 if (c == '-')
1213 { c = follow('>', EQUIV, '-');
1214 if (c == '-')
1215 { Ungetch(c);
1216 c = '<';
1217 }
1218 } else
1219 { Ungetch(c);
1220 c = '<';
1221 } }
1222 default: break;
1223 } }
1224
1225 switch (c) {
1226 case '/': c = follow('*', 0, '/');
1227 if (!c) { in_comment = 1; goto again; }
1228 break;
1229 case '*': c = follow('/', 0, '*');
1230 if (!c) { in_comment = 0; goto again; }
1231 break;
1232 case ':': c = follow(':', SEP, ':'); break;
1233 case '-': c = follow('>', SEMI, follow('-', DECR, '-')); break;
1234 case '+': c = follow('+', INCR, '+'); break;
1235 case '<': c = follow('<', LSHIFT, follow('=', LE, LT)); break;
1236 case '>': c = follow('>', RSHIFT, follow('=', GE, GT)); break;
1237 case '=': c = follow('=', EQ, ASGN); break;
1238 case '!': c = follow('=', NE, follow('!', O_SND, SND)); break;
1239 case '?': c = follow('?', R_RCV, RCV); break;
1240 case '&': c = follow('&', AND, '&'); break;
1241 case '|': c = follow('|', OR, '|'); break;
1242 case ';': c = SEMI; break;
1243 case '.': c = follow('.', DOTDOT, '.'); break;
1244 case '{': scope_seq[scope_level++]++; set_cur_scope(); break;
1245 case '}': scope_level--; set_cur_scope(); break;
1246 default : break;
1247 }
1248 Token(c)
1249 }
1250
1251 static struct {
1252 char *s; int tok;
1253 } LTL_syms[] = {
1254 /* [], <>, ->, and <-> are intercepted in lex() */
1255 { "U", UNTIL },
1256 { "V", RELEASE },
1257 { "W", WEAK_UNTIL },
1258 { "X", NEXT },
1259 { "always", ALWAYS },
1260 { "eventually", EVENTUALLY },
1261 { "until", UNTIL },
1262 { "stronguntil",UNTIL },
1263 { "weakuntil", WEAK_UNTIL },
1264 { "release", RELEASE },
1265 { "next", NEXT },
1266 { "implies", IMPLIES },
1267 { "equivalent", EQUIV },
1268 { 0, 0 },
1269 };
1270
1271 static struct {
1272 char *s; int tok; int val; char *sym;
1273 } Names[] = {
1274 {"active", ACTIVE, 0, 0},
1275 {"assert", ASSERT, 0, 0},
1276 {"atomic", ATOMIC, 0, 0},
1277 {"bit", TYPE, BIT, 0},
1278 {"bool", TYPE, BIT, 0},
1279 {"break", BREAK, 0, 0},
1280 {"byte", TYPE, BYTE, 0},
1281 {"c_code", C_CODE, 0, 0},
1282 {"c_decl", C_DECL, 0, 0},
1283 {"c_expr", C_EXPR, 0, 0},
1284 {"c_state", C_STATE, 0, 0},
1285 {"c_track", C_TRACK, 0, 0},
1286 {"D_proctype", D_PROCTYPE, 0, 0},
1287 {"do", DO, 0, 0},
1288 {"chan", TYPE, CHAN, 0},
1289 {"else", ELSE, 0, 0},
1290 {"empty", EMPTY, 0, 0},
1291 {"enabled", ENABLED, 0, 0},
1292 {"eval", EVAL, 0, 0},
1293 {"false", CONST, 0, 0},
1294 {"fi", FI, 0, 0},
1295 {"for", FOR, 0, 0},
1296 {"full", FULL, 0, 0},
1297 {"goto", GOTO, 0, 0},
1298 {"hidden", HIDDEN, 0, ":hide:"},
1299 {"if", IF, 0, 0},
1300 {"in", IN, 0, 0},
1301 {"init", INIT, 0, ":init:"},
1302 {"inline", INLINE, 0, 0},
1303 {"int", TYPE, INT, 0},
1304 {"len", LEN, 0, 0},
1305 {"local", ISLOCAL, 0, ":local:"},
1306 {"ltl", LTL, 0, ":ltl:"},
1307 {"mtype", TYPE, MTYPE, 0},
1308 {"nempty", NEMPTY, 0, 0},
1309 {"never", CLAIM, 0, ":never:"},
1310 {"nfull", NFULL, 0, 0},
1311 {"notrace", TRACE, 0, ":notrace:"},
1312 {"np_", NONPROGRESS, 0, 0},
1313 {"od", OD, 0, 0},
1314 {"of", OF, 0, 0},
1315 {"pc_value", PC_VAL, 0, 0},
1316 {"pid", TYPE, BYTE, 0},
1317 {"printf", PRINT, 0, 0},
1318 {"printm", PRINTM, 0, 0},
1319 {"priority", PRIORITY, 0, 0},
1320 {"proctype", PROCTYPE, 0, 0},
1321 {"provided", PROVIDED, 0, 0},
1322 {"run", RUN, 0, 0},
1323 {"d_step", D_STEP, 0, 0},
1324 {"select", SELECT, 0, 0},
1325 {"short", TYPE, SHORT, 0},
1326 {"skip", CONST, 1, 0},
1327 {"timeout", TIMEOUT, 0, 0},
1328 {"trace", TRACE, 0, ":trace:"},
1329 {"true", CONST, 1, 0},
1330 {"show", SHOW, 0, ":show:"},
1331 {"typedef", TYPEDEF, 0, 0},
1332 {"unless", UNLESS, 0, 0},
1333 {"unsigned", TYPE, UNSIGNED, 0},
1334 {"xr", XU, XR, 0},
1335 {"xs", XU, XS, 0},
1336 {0, 0, 0, 0},
1337 };
1338
1339 static int
check_name(char * s)1340 check_name(char *s)
1341 { int i;
1342
1343 yylval = nn(ZN, 0, ZN, ZN);
1344
1345 if (ltl_mode)
1346 { for (i = 0; LTL_syms[i].s; i++)
1347 { if (strcmp(s, LTL_syms[i].s) == 0)
1348 { return LTL_syms[i].tok;
1349 } } }
1350
1351 for (i = 0; Names[i].s; i++)
1352 { if (strcmp(s, Names[i].s) == 0)
1353 { yylval->val = Names[i].val;
1354 if (Names[i].sym)
1355 yylval->sym = lookup(Names[i].sym);
1356 return Names[i].tok;
1357 } }
1358
1359 if ((yylval->val = ismtype(s)) != 0)
1360 { yylval->ismtyp = 1;
1361 return CONST;
1362 }
1363
1364 if (strcmp(s, "_last") == 0)
1365 has_last++;
1366
1367 if (Inlining >= 0 && !ReDiRect)
1368 { Lextok *tt, *t = Inline_stub[Inlining]->params;
1369
1370 for (i = 0; t; t = t->rgt, i++) /* formal pars */
1371 if (!strcmp(s, t->lft->sym->name) /* varname matches formal */
1372 && strcmp(s, Inline_stub[Inlining]->anms[i]) != 0) /* actual pars */
1373 {
1374 #if 0
1375 if (verbose&32)
1376 printf("\tline %d, replace %s in call of '%s' with %s\n",
1377 lineno, s,
1378 Inline_stub[Inlining]->nm->name,
1379 Inline_stub[Inlining]->anms[i]);
1380 #endif
1381 for (tt = Inline_stub[Inlining]->params; tt; tt = tt->rgt)
1382 if (!strcmp(Inline_stub[Inlining]->anms[i],
1383 tt->lft->sym->name))
1384 { /* would be cyclic if not caught */
1385 printf("spin: %s:%d replacement value: %s\n",
1386 oFname->name?oFname->name:"--", lineno, tt->lft->sym->name);
1387 fatal("formal par of %s contains replacement value",
1388 Inline_stub[Inlining]->nm->name);
1389 yylval->ntyp = tt->lft->ntyp;
1390 yylval->sym = lookup(tt->lft->sym->name);
1391 return NAME;
1392 }
1393
1394 /* check for occurrence of param as field of struct */
1395 { char *ptr = Inline_stub[Inlining]->anms[i];
1396 while ((ptr = strstr(ptr, s)) != NULL)
1397 { if (*(ptr-1) == '.'
1398 || *(ptr+strlen(s)) == '.')
1399 { fatal("formal par of %s used in structure name",
1400 Inline_stub[Inlining]->nm->name);
1401 }
1402 ptr++;
1403 } }
1404 ReDiRect = Inline_stub[Inlining]->anms[i];
1405 return 0;
1406 } }
1407
1408 yylval->sym = lookup(s); /* symbol table */
1409 if (isutype(s))
1410 return UNAME;
1411 if (isproctype(s))
1412 return PNAME;
1413 if (iseqname(s))
1414 return INAME;
1415
1416 return NAME;
1417 }
1418
1419 int
yylex(void)1420 yylex(void)
1421 { static int last = 0;
1422 static int hold = 0;
1423 int c;
1424 /*
1425 * repair two common syntax mistakes with
1426 * semi-colons before or after a '}'
1427 */
1428 if (hold)
1429 { c = hold;
1430 hold = 0;
1431 } else
1432 { c = lex();
1433 if (last == ELSE
1434 && c != SEMI
1435 && c != FI)
1436 { hold = c;
1437 last = 0;
1438 return SEMI;
1439 }
1440 if (last == '}'
1441 && c != PROCTYPE
1442 && c != INIT
1443 && c != CLAIM
1444 && c != SEP
1445 && c != FI
1446 && c != OD
1447 && c != '}'
1448 && c != UNLESS
1449 && c != SEMI
1450 && c != EOF)
1451 { hold = c;
1452 last = 0;
1453 return SEMI; /* insert ';' */
1454 }
1455 if (c == SEMI)
1456 { /* if context, we're not in a typedef
1457 * because they're global.
1458 * if owner, we're at the end of a ref
1459 * to a struct field -- prevent that the
1460 * lookahead is interpreted as a field of
1461 * the same struct...
1462 */
1463 if (context) owner = ZS;
1464 hold = lex(); /* look ahead */
1465 if (hold == '}'
1466 || hold == SEMI)
1467 { c = hold; /* omit ';' */
1468 hold = 0;
1469 }
1470 }
1471 }
1472 last = c;
1473
1474 if (IArgs)
1475 { static int IArg_nst = 0;
1476
1477 if (strcmp(yytext, ",") == 0)
1478 { IArg_cont[++IArgno][0] = '\0';
1479 } else if (strcmp(yytext, "(") == 0)
1480 { if (IArg_nst++ == 0)
1481 { IArgno = 0;
1482 IArg_cont[0][0] = '\0';
1483 } else
1484 strcat(IArg_cont[IArgno], yytext);
1485 } else if (strcmp(yytext, ")") == 0)
1486 { if (--IArg_nst > 0)
1487 strcat(IArg_cont[IArgno], yytext);
1488 } else if (c == CONST && yytext[0] == '\'')
1489 { sprintf(yytext, "'%c'", yylval->val);
1490 strcat(IArg_cont[IArgno], yytext);
1491 } else if (c == CONST)
1492 { sprintf(yytext, "%d", yylval->val);
1493 strcat(IArg_cont[IArgno], yytext);
1494 } else
1495 {
1496 switch (c) {
1497 case SEP: strcpy(yytext, "::"); break;
1498 case SEMI: strcpy(yytext, ";"); break;
1499 case DECR: strcpy(yytext, "--"); break;
1500 case INCR: strcpy(yytext, "++"); break;
1501 case LSHIFT: strcpy(yytext, "<<"); break;
1502 case RSHIFT: strcpy(yytext, ">>"); break;
1503 case LE: strcpy(yytext, "<="); break;
1504 case LT: strcpy(yytext, "<"); break;
1505 case GE: strcpy(yytext, ">="); break;
1506 case GT: strcpy(yytext, ">"); break;
1507 case EQ: strcpy(yytext, "=="); break;
1508 case ASGN: strcpy(yytext, "="); break;
1509 case NE: strcpy(yytext, "!="); break;
1510 case R_RCV: strcpy(yytext, "??"); break;
1511 case RCV: strcpy(yytext, "?"); break;
1512 case O_SND: strcpy(yytext, "!!"); break;
1513 case SND: strcpy(yytext, "!"); break;
1514 case AND: strcpy(yytext, "&&"); break;
1515 case OR: strcpy(yytext, "||"); break;
1516 }
1517 strcat(IArg_cont[IArgno], yytext);
1518 }
1519 }
1520 return c;
1521 }
1522