1 /***** spin: spinlex.c *****/
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
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 */
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 */
34 typedef struct C_Added {
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;
54 int scope_seq[128], scope_level = 0;
55 char CurScope[MAXSCOPESZ];
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;
68 #define ValToken(x, y) { if (in_comment) goto again; \
69 yylval = nn(ZN,0,ZN,ZN); \
75 #define SymToken(x, y) { if (in_comment) goto again; \
76 yylval = nn(ZN,0,ZN,ZN); \
82 static int getinline(void);
83 static void uninline(void);
86 static int PushedBack;
87 static char pushedback[4096];
92 if (PushedBack + strlen(s) > 4094)
93 { fatal("select statement too large", 0);
95 strcat(pushedback, s);
96 PushedBack += strlen(s);
103 if (PushedBack > 0 && PushBack < PushedBack)
104 { c = pushedback[PushBack++];
105 if (PushBack == PushedBack)
106 { pushedback[0] = '\0';
107 PushBack = PushedBack = 0;
109 return c; /* expanded select statement */
118 { printf("<%c:%d>[%d] ", c, c, Inlining);
129 if (PushedBack > 0 && PushBack > 0)
140 { printf("\n<bs{%d}bs>\n", c);
146 { return (c != '$' && c != '\n');
151 { return (c != '\"' && c != '\n');
156 { return (isalnum(c) || c == '_');
161 { return isalpha(c); /* could be macro */
166 { return isdigit(c); /* could be macro */
170 getword(int first, int (*tst)(int))
173 yytext[i++]= (char) first;
174 while (tst(c = Getchar()))
175 { yytext[i++] = (char) c;
178 yytext[i++] = (char) c; /* no tst */
186 follow(int tok, int ifyes, int ifno)
189 if ((c = Getchar()) == tok)
197 static IType *seqnames;
200 def_inline(Symbol *s, int ln, char *ptr, char *prc, Lextok *nms)
203 char *nw = (char *) emalloc(strlen(ptr)+1);
206 for (tmp = seqnames; tmp; cnt++, tmp = tmp->nxt)
207 if (!strcmp(s->name, tmp->nm->name))
208 { non_fatal("procedure name %s redefined",
210 tmp->cn = (Lextok *) nw;
216 tmp = (IType *) emalloc(sizeof(IType));
218 tmp->cn = (Lextok *) nw;
221 { tmp->prec = (char *) emalloc(strlen(prc)+1);
222 strcpy(tmp->prec, prc);
226 tmp->uiid = cnt+1; /* so that 0 means: not an inline */
232 gencodetable(FILE *fd)
237 if (separate == 2) return;
239 fprintf(fd, "struct {\n");
240 fprintf(fd, " char *c; char *t;\n");
241 fprintf(fd, "} code_lookup[] = {\n");
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\", ",
249 q = (char *) tmp->cn;
251 while (*q == '\n' || *q == '\r' || *q == '\\')
256 while (*q && cnt < 1024) /* pangen1.h allows 2048 */
273 if (*q) fprintf(fd, "...");
275 fprintf(fd, " },\n");
278 fprintf(fd, " { (char *) 0, \"\" }\n");
286 for (tmp = seqnames; tmp; tmp = tmp->nxt)
287 { if (!strcmp(t, tmp->nm->name))
294 return_statement(Lextok *n)
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);
302 { fatal("return statement outside inline", (char *) 0);
314 { ReDiRect = (char *) 0;
315 c = *Inliner[Inlining]++;
319 c = *Inliner[Inlining]++;
324 lineno = Inline_stub[Inlining]->cln;
325 Fname = Inline_stub[Inlining]->cfn;
330 printf("spin: %s:%d, done inlining %s\n",
331 Fname, lineno, Inline_stub[Inlining+1]->nm->name);
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;
361 for (tmp = seqnames; tmp; tmp = tmp->nxt)
362 if (!strcmp(s, tmp->nm->name))
365 fatal("cannot happen, missing inline def %s", s);
371 c_state(Symbol *s, Symbol *t, Symbol *ival) /* name, scope, ival */
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" */
382 if(strncmp(r->s->name, "\"unsigned unsigned", 18) == 0)
384 for (i = 10; i < 18; i++)
385 { r->s->name[i] = ' ';
387 /* printf("corrected <%s>\n", r->s->name); */
393 c_track(Symbol *s, Symbol *t, Symbol *stackonly) /* name, size */
396 r = (C_Added *) emalloc(sizeof(C_Added));
399 r->ival = stackonly; /* abuse of name */
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);
413 has_stack = 1; /* unmatched stack */
421 { while (*p == ' ' || *p == '\t')
424 { fatal("bad format - 1", (char *) 0);
430 skip_nonwhite(char *p)
433 { while (*p != ' ' && *p != '\t')
436 { fatal("bad format - 2", (char *) 0);
443 { char *op = r->s->name;
445 char *q = (char *) 0;
447 Symbol *ofnm = Fname;
449 /* try to get the type separated from the name */
453 p = skip_white(p); /* initial white space */
455 if (strncmp(p, "enum", strlen("enum")) == 0) /* special case: a two-part typename */
456 { p += strlen("enum")+1;
459 if (strncmp(p, "unsigned", strlen("unsigned")) == 0) /* possibly a two-part typename */
460 { p += strlen("unsigned")+1;
461 q = p = skip_white(p);
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 */
470 { p = q; /* unsigned with implied 'int' */
472 { fatal("c_state format (%s)", op);
475 if (strchr(p, '[') && !strchr(p, '{'))
476 { non_fatal("array initialization error, c_state (%s)", p);
487 c_add_globinit(FILE *fd)
491 fprintf(fd, "void\nglobinit(void)\n{\n");
492 for (r = c_added; r; r = r->nxt)
496 if (strncmp(r->t->name, " Global ", strlen(" Global ")) == 0)
497 { for (q = r->ival->name; *q; q++)
501 *q++ = ' '; /* skip over the next */
503 p = jump_etc(r); /* e.g., "int **q" */
505 fprintf(fd, " now.%s = %s;\n", p, r->ival->name);
508 if (strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) == 0)
509 { for (q = r->ival->name; *q; q++)
513 *q++ = ' '; /* skip over the next */
515 p = jump_etc(r); /* e.g., "int **q" */
517 fprintf(fd, " %s = %s;\n", p, r->ival->name); /* no now. prefix */
524 c_add_locinit(FILE *fd, int tpnr, char *pnm)
529 fprintf(fd, "void\nlocinit%d(int h)\n{\n", tpnr);
530 for (r = c_added; r; r = r->nxt)
532 && strncmp(r->t->name, " Local", strlen(" Local")) == 0)
533 { for (q = r->ival->name; *q; q++)
537 p = jump_etc(r); /* e.g., "int **q" */
539 q = r->t->name + strlen(" Local");
540 while (*q == ' ' || *q == '\t')
541 q++; /* process name */
543 s = (char *) emalloc(strlen(q)+1);
547 while (*q == ' ' || *q == '\t')
550 if (strcmp(pnm, s) != 0)
554 { fprintf(fd, "\tuchar *this = pptr(h);\n");
559 { fprintf(fd, "\t\t((P%d *)this)->%s = %s;\n",
560 tpnr, p, r->ival->name);
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
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 */
591 c_add_sv(FILE *fd) /* 1+2 -- called in pangen1.c */
595 if (!c_added && !c_tracked) return 0;
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);
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 */
608 for (r = c_tracked; r; r = r->nxt)
609 cnt++; /* preferred use */
611 if (cnt == 0) return 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);
624 for (r = c_tracked; r; r = r->nxt)
625 { if (r->ival != ZS) continue;
628 (cnt==0)?"":"+", r->t->name);
632 if (cnt == 0) fprintf(fd, "4"); /* now redundant */
638 c_stack_size(FILE *fd)
642 for (r = c_tracked; r; r = r->nxt)
644 { fprintf(fd, "%s%s",
645 (cnt==0)?"":"+", r->t->name);
654 c_add_stack(FILE *fd)
658 if ((!c_added && !c_tracked) || !has_stack)
662 for (r = c_tracked; r; r = r->nxt)
668 { fprintf(fd, " uchar c_stack[StackSize];\n");
673 c_add_hidden(FILE *fd)
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] = '"';
682 /* called before c_add_def - quotes are still there */
686 c_add_loc(FILE *fd, char *s) /* state vector entries for proctype s */
688 static char buf[1024];
691 if (!c_added) return;
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')
701 if (strcmp(p, buf) == 0)
702 fprintf(fd, " %s;\n", r->s->name);
706 c_add_def(FILE *fd) /* 3 - called in plunk_c_fcts() */
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 */
714 r->t->name[strlen(r->t->name)-1] = ' ';
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)
722 if (strchr(r->s->name, '&'))
723 fatal("dereferencing state object: %s", r->s->name);
725 fprintf(fd, "extern %s %s;\n", r->t->name, r->s->name);
727 for (r = c_tracked; r; r = r->nxt)
728 { r->s->name[strlen(r->s->name)-1] = ' ';
729 r->s->name[0] = ' '; /* remove " */
731 r->t->name[strlen(r->t->name)-1] = ' ';
736 { fprintf(fd, "#endif\n");
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;
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",
755 fprintf(fd, "\tp_t_r += %s;\n", r->t->name);
757 fprintf(fd, "}\n\n");
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)
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);
775 for (r = c_tracked; r; r = r->nxt)
776 { if (r->ival) continue;
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",
784 fprintf(fd, "\tp_t_r += %s;\n", r->t->name);
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;
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);
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)
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);
819 for (r = c_tracked; r; r = r->nxt)
820 { if (r->ival != ZS) continue;
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);
829 fprintf(fd, "#endif\n");
833 plunk_reverse(FILE *fd, IType *p, int matchthis)
837 plunk_reverse(fd, p->nxt, matchthis);
840 && p->nm->type == matchthis
842 { fprintf(fd, "\n/* start of %s */\n", p->nm->name);
844 while (*z == '\n' || *z == '\r' || *z == '\\')
847 /* e.g.: \#include "..." */
850 while ((y = strstr(y, "\\#")) != NULL)
854 fprintf(fd, "%s\n", z);
855 fprintf(fd, "\n/* end of %s */\n", p->nm->name);
860 plunk_c_decls(FILE *fd)
862 plunk_reverse(fd, seqnames, CODE_DECL);
866 plunk_c_fcts(FILE *fd)
868 if (separate == 2 && hastrack)
874 plunk_reverse(fd, seqnames, CODE_FRAG);
876 if (c_added || c_tracked) /* enables calls to c_revert and c_update */
877 fprintf(fd, "#define C_States 1\n");
879 fprintf(fd, "#undef C_States\n");
889 check_inline(IType *tmp)
895 for (p = rdy; p; p = p->nxt)
896 { if (strcmp(p->n->name, X->n->name) == 0)
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);
910 plunk_expr(FILE *fd, char *s)
914 tmp = find_inline(s);
918 { for (q = (char *) tmp->cn; q && *q != '\0'; q++)
923 fprintf(fd, "%c", *q);
926 { fprintf(fd, "%s", (char *) tmp->cn);
931 preruse(FILE *fd, Lextok *n) /* check a condition for c_expr with preconditions */
935 if (n->ntyp == C_EXPR)
936 { tmp = find_inline(n->sym->name);
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\"); ",
944 fprintf(fd, "_m = 3; goto P999; } } \n\t\t");
947 { preruse(fd, n->rgt);
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 */
964 put_inline(FILE *fd, char *s)
967 tmp = find_inline(s);
969 return (char *) tmp->cn;
976 { seqnames->is_expr = 1;
981 plunk_inline(FILE *fd, char *s, int how, int gencode) /* c_code with precondition */
984 tmp = find_inline(s);
988 if (how && tmp->prec)
989 { fprintf(fd, "if (!(%s)) { if (!readtrail) {",
991 fprintf(fd, " uerror(\"c_code line %d precondition false: %s\"); continue; ",
994 fprintf(fd, "} else { ");
995 fprintf(fd, "printf(\"pan: precondition false: %s\\n\"); _m = 3; goto P999; } } ",
999 if (!gencode) /* not in d_step */
1000 { fprintf(fd, "\n\t\tsv_save();");
1003 fprintf(fd, "%s", (char *) tmp->cn);
1004 fprintf(fd, " }\n");
1008 side_scan(char *t, char *pat)
1009 { char *r = strstr(t, pat);
1016 no_side_effects(char *s)
1020 /* could still defeat this check via hidden
1021 * side effects in function calls,
1022 * but this will catch at least some cases
1025 tmp = find_inline(s);
1026 t = (char *) tmp->cn;
1028 if (side_scan(t, ";")
1029 || side_scan(t, "++")
1030 || side_scan(t, "--"))
1032 bad: lineno = tmp->dln;
1034 non_fatal("c_expr %s has side-effects", s);
1037 while ((t = strchr(t, '=')) != NULL)
1054 pickup_inline(Symbol *t, Lextok *apars, Lextok *rval)
1055 { IType *tmp; Lextok *p, *q; int j;
1057 tmp = find_inline(t->name);
1059 if (++Inlining >= MAXINL)
1060 fatal("inlines nested too deeply", 0);
1061 tmp->cln = lineno; /* remember calling point */
1062 tmp->cfn = Fname; /* and filename */
1065 for (p = apars, q = tmp->params, j = 0; p && q; p = p->rgt, q = q->rgt)
1066 j++; /* count them */
1068 fatal("wrong nr of params on call of '%s'", t->name);
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]);
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;
1082 printf("spin: %s:%d, inlining '%s' (from %s:%d)\n",
1083 tmp->cfn->name, tmp->cln, t->name, tmp->dfn->name, tmp->dln);
1085 for (j = 0; j < Inlining; j++)
1086 { if (Inline_stub[j] == Inline_stub[Inlining])
1087 { fatal("cyclic inline attempt on: %s", t->name);
1089 last_token = SEMI; /* avoid insertion of extra semi */
1095 do_directive(int first)
1096 { int c = first; /* handles lines starting with pound */
1098 getword(c, isalpha_);
1100 if (strcmp(yytext, "#ident") == 0)
1103 if ((c = Getchar()) != ' ')
1104 fatal("malformed preprocessor directive - # .", 0);
1106 if (!isdigit_(c = Getchar()))
1107 fatal("malformed preprocessor directive - # .lineno", 0);
1109 getword(c, isdigit_);
1110 lineno = atoi(yytext); /* pickup the line number */
1112 if ((c = Getchar()) == '\n')
1113 return; /* no filename */
1116 fatal("malformed preprocessor directive - .fname", 0);
1118 if ((c = Getchar()) != '\"')
1119 { printf("got %c, expected \" -- lineno %d\n", c, lineno);
1120 fatal("malformed preprocessor directive - .fname (%s)", yytext);
1123 getword(Getchar(), notquote); /* was getword(c, notquote); */
1124 if (Getchar() != '\"')
1125 fatal("malformed preprocessor directive - fname.", 0);
1127 /* strcat(yytext, "\""); */
1128 Fname = lookup(yytext);
1130 while (Getchar() != '\n')
1135 precondition(char *q)
1156 fatal("cannot happen", (char *) 0); /* unreachable */
1161 prep_inline(Symbol *s, Lextok *nms)
1162 { int c, nest = 1, dln, firstchar, cnr;
1165 static char Buf1[SOMETHINGBIG], Buf2[RATHERSMALL];
1166 static int c_code = 1;
1168 for (t = nms; t; t = t->rgt)
1170 { if (t->lft->ntyp != NAME)
1171 fatal("bad param to inline %s", s?s->name:"--");
1172 t->lft->sym->hidden |= 32;
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;
1191 if (s->type != CODE_FRAG)
1193 precondition(&Buf2[0]); /* e.g., c_code [p] { r = p-r; } */
1200 case ' ': case '\t': case '\f': case '\r':
1203 printf("spin: saw char '%c'\n", c);
1204 bad: fatal("bad inline: %s", s->name);
1209 if (s->type == CODE_FRAG)
1211 { sprintf(Buf1, "\t/* line %d %s */\n\t\t",
1212 lineno, Fname->name);
1217 { sprintf(Buf1, "\n#line %d \"%s\"\n{", lineno, Fname->name);
1222 cnr = 1; /* not zero */
1226 if (p - Buf1 >= SOMETHINGBIG)
1227 fatal("inline text too long", 0);
1241 if (s->type == CODE_FRAG)
1242 { *--p = '\0'; /* remove trailing '}' */
1244 def_inline(s, dln, &Buf1[0], &Buf2[0], nms);
1246 { printf("%3d: %s, warning: empty inline definition (%s)\n",
1247 dln, Fname->name, s->name);
1249 return s; /* normal return */
1255 do_directive(c); /* reads to newline */
1271 { *p++ = (char) Getchar();
1273 if (p - Buf1 >= SOMETHINGBIG)
1274 { fatal("inline text too long", 0);
1276 } while (c != '"'); /* end of string */
1283 { *p++ = (char) Getchar();
1302 strcpy(CurScope, "_");
1305 for (i = 0; i < scope_level; i++)
1306 { sprintf(tmpbuf, "%d_", scope_seq[i]);
1307 strcat(CurScope, tmpbuf);
1317 while ((c = Getchar()) != '\n' && c != EOF)
1318 { b[i++] = (char) c;
1321 yylval = nn(ZN, 0, ZN, ZN);
1322 yylval->sym = lookup(b);
1326 static int specials[] = {
1328 OD, FI, ELSE, BREAK,
1329 C_CODE, C_EXPR, C_DECL,
1330 NAME, CONST, INCR, DECR, 0
1334 follows_token(int c)
1337 for (i = 0; specials[i]; i++)
1338 { if (c == specials[i])
1345 /* defer ltl formula to the end of the spec
1346 * no matter where they appear in the original
1349 static int deferred = 0;
1350 static FILE *defer_fd;
1356 { return 0; /* nothing was deferred */
1360 defer_fd = fopen(TMP_FILE2, "r");
1362 { non_fatal("cannot retrieve deferred ltl formula", (char *) 0);
1373 (void) unlink(TMP_FILE2);
1380 { defer_fd = fopen(TMP_FILE2, "w+");
1382 { non_fatal("cannot defer ltl expansion", (char *) 0);
1385 fprintf(defer_fd, "ltl ");
1387 while ((c = getc(yyin)) != EOF)
1396 fprintf(defer_fd, "%c", c);
1398 fprintf(defer_fd, "}\n");
1404 #define EXPAND_SELECT
1405 #ifdef EXPAND_SELECT
1406 static char tmp_hold[256];
1411 { tmp_hold[0] = '\0';
1416 scan_to(int stop, int (*tst)(int), char *buf)
1420 if (tmp_has < sizeof(tmp_hold))
1421 { tmp_hold[tmp_has++] = c;
1428 if (tst && !tst(c) && c != ' ' && c != '\t')
1431 } while (c != stop && c != EOF);
1439 { printf("saw: '%c', expected '%c'\n", c, stop);
1441 if (tmp_has < sizeof(tmp_hold))
1442 { tmp_hold[tmp_has] = '\0';
1443 push_back(tmp_hold);
1445 { printf("pushed back: <'%s'>\n", tmp_hold);
1447 return 0; /* internal expansion fails */
1449 { fatal("expecting select ( name : constant .. constant )", 0);
1451 return 1; /* success */
1460 yytext[0] = (char) c;
1475 case '\n': /* newline */
1477 /* make most semi-colons optional */
1482 && follows_token(last_token))
1484 { printf("insert ; line %d, last_token %d in_seq %d\n",
1485 lineno-1, last_token, in_seq);
1489 /* else fall thru */
1490 case '\r': /* carriage return */
1493 case ' ': case '\t': case '\f': /* white space */
1496 case '#': /* preprocessor directive */
1497 if (in_comment) goto again;
1499 { last_token = PREPROC;
1506 getword(c, notquote);
1507 if (Getchar() != '\"')
1508 fatal("string not terminated", yytext);
1509 strcat(yytext, "\"");
1510 SymToken(lookup(yytext), STRING)
1513 getword('\"', notdollar);
1514 if (Getchar() != '$')
1515 fatal("ltl definition not terminated", yytext);
1516 strcat(yytext, "\"");
1517 SymToken(lookup(yytext), STRING)
1519 case '\'': /* new 3.0.9 */
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';
1528 if (Getchar() != '\'' && !in_comment)
1529 fatal("character quote missing: %s", yytext);
1538 getword(c, isdigit_);
1540 nr = strtol(yytext, NULL, 10);
1542 { fprintf(stderr, "spin: value out of range: '%s' read as '%d'\n",
1545 ValToken((int)nr, CONST)
1548 if (isalpha_(c) || c == '_')
1549 { getword(c, isalnum_);
1551 { c = check_name(yytext);
1553 #ifdef EXPAND_SELECT
1554 if (c == SELECT && Inlining < 0)
1555 { char name[64], from[32], upto[32];
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;
1568 { printf("Select %s from %d to %d\n",
1572 { non_fatal("bad range in select statement", 0);
1577 for (i = a; i <= b; i++)
1580 sprintf(buf, "%s = %d ",
1587 sprintf(buf, "%s = %d; do ",
1590 sprintf(buf, ":: (%s < %d) -> %s++ ",
1593 push_back(":: break od; ");
1601 if (c == LTL && !deferred)
1602 { if (put_deferred())
1610 /* else fall through */
1617 case '-': c = follow('>', IMPLIES, '-'); break;
1618 case '[': c = follow(']', ALWAYS, '['); break;
1619 case '<': c = follow('>', EVENTUALLY, '<');
1623 { c = follow('>', EQUIV, '-');
1636 case '/': c = follow('*', 0, '/');
1637 if (!c) { in_comment = 1; goto again; }
1639 case '*': c = follow('/', 0, '*');
1640 if (!c) { in_comment = 0; goto again; }
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;
1664 /* [], <>, ->, and <-> are intercepted in lex() */
1667 { "W", WEAK_UNTIL },
1669 { "always", ALWAYS },
1670 { "eventually", EVENTUALLY },
1672 { "stronguntil",UNTIL },
1673 { "weakuntil", WEAK_UNTIL },
1674 { "release", RELEASE },
1676 { "implies", IMPLIES },
1677 { "equivalent", EQUIV },
1682 char *s; int tok; int val; char *sym;
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},
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},
1706 {"full", FULL, 0, 0},
1707 {"get_priority", GET_P, 0, 0},
1708 {"goto", GOTO, 0, 0},
1709 {"hidden", HIDDEN, 0, ":hide:"},
1712 {"init", INIT, 0, ":init:"},
1713 {"inline", INLINE, 0, 0},
1714 {"int", TYPE, INT, 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},
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},
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},
1756 yylval = nn(ZN, 0, ZN, ZN);
1759 { for (i = 0; LTL_syms[i].s; i++)
1760 { if (strcmp(s, LTL_syms[i].s) == 0)
1761 { return LTL_syms[i].tok;
1764 for (i = 0; Names[i].s; i++)
1765 { if (strcmp(s, Names[i].s) == 0)
1766 { yylval->val = Names[i].val;
1768 yylval->sym = lookup(Names[i].sym);
1769 if (Names[i].tok == IN && !in_for)
1772 return Names[i].tok;
1775 if ((yylval->val = ismtype(s)) != 0)
1776 { yylval->ismtyp = 1;
1780 if (strcmp(s, "_last") == 0)
1783 if (strcmp(s, "_priority") == 0)
1786 if (Inlining >= 0 && !ReDiRect)
1787 { Lextok *tt, *t = Inline_stub[Inlining]->params;
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 */
1795 printf("\tline %d, replace %s in call of '%s' with %s\n",
1797 Inline_stub[Inlining]->nm->name,
1798 Inline_stub[Inlining]->anms[i]);
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);
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);
1823 ReDiRect = Inline_stub[Inlining]->anms[i];
1827 yylval->sym = lookup(s); /* symbol table */
1840 { static int last = 0;
1841 static int hold = 0;
1844 * repair two common syntax mistakes with
1845 * semi-colons before or after a '}'
1877 return SEMI; /* insert ';' */
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...
1887 if (context) owner = ZS;
1888 hold = lex(); /* look ahead */
1892 { c = hold; /* omit ';' */
1900 { static int IArg_nst = 0;
1902 if (strcmp(yytext, ",") == 0)
1903 { IArg_cont[++IArgno][0] = '\0';
1904 } else if (strcmp(yytext, "(") == 0)
1905 { if (IArg_nst++ == 0)
1907 IArg_cont[0][0] = '\0';
1909 { assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont));
1910 strcat(IArg_cont[IArgno], yytext);
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);
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);
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;
1949 assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont));
1950 strcat(IArg_cont[IArgno], yytext);