1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283848586878889909192939495969798991001011021031041051061071081091101111121131141151161171181191201211221231241251261271281291301311321331341351361371381391401411421431441451461471481491501511521531541551561571581591601611621631641651661671681691701711721731741751761771781791801811821831841851861871881891901911921931941951961971981992002012022032042052062072082092102112122132142152162172182192202212222232242252262272282292302312322332342352362372382392402412422432442452462472482492502512522532542552562572582592602612622632642652662672682692702712722732742752762772782792802812822832842852862872882892902912922932942952962972982993003013023033043053063073083093103113123133143153163173183193203213223233243253263273283293303313323333343353363373383393403413423433443453463473483493503513523533543553563573583593603613623633643653663673683693703713723733743753763773783793803813823833843853863873883893903913923933943953963973983994004014024034044054064074084094104114124134144154164174184194204214224234244254264274284294304314324334344354364374384394404414424434444454464474484494504514524534544554564574584594604614624634644654664674684694704714724734744754764774784794804814824834844854864874884894904914924934944954964974984995005015025035045055065075085095105115125135145155165175185195205215225235245255265275285295305315325335345355365375385395405415425435445455465475485495505515525535545555565575585595605615625635645655665675685695705715725735745755765775785795805815825835845855865875885895905915925935945955965975985996006016026036046056066076086096106116126136146156166176186196206216226236246256266276286296306316326336346356366376386396406416426436446456466476486496506516526536546556566576586596606616626636646656666676686696706716726736746756766776786796806816826836846856866876886896906916926936946956966976986997007017027037047057067077087097107117127137147157167177187197207217227237247257267277287297307317327337347357367377387397407417427437447457467477487497507517527537547557567577587597607617627637647657667677687697707717727737747757767777787797807817827837847857867877887897907917927937947957967977987998008018028038048058068078088098108118128138148158168178188198208218228238248258268278288298308318328338348358368378388398408418428438448458468478488498508518528538548558568578588598608618628638648658668678688698708718728738748758768778788798808818828838848858868878888898908918928938948958968978988999009019029039049059069079089099109119129139149159169179189199209219229239249259269279289299309319329339349359369379389399409419429439449459469479489499509519529539549559569579589599609619629639649659669679689699709719729739749759769779789799809819829839849859869879889899909919929939949959969979989991000100110021003100410051006100710081009101010111012101310141015101610171018101910201021102210231024102510261027102810291030103110321033103410351036103710381039104010411042104310441045104610471048104910501051105210531054105510561057105810591060106110621063106410651066106710681069107010711072107310741075107610771078107910801081108210831084108510861087108810891090109110921093109410951096109710981099110011011102110311041105110611071108110911101111111211131114111511161117111811191120112111221123112411251126112711281129113011311132113311341135113611371138113911401141114211431144114511461147114811491150115111521153115411551156115711581159116011611162116311641165116611671168116911701171117211731174117511761177117811791180118111821183118411851186118711881189119011911192119311941195119611971198119912001201120212031204120512061207120812091210121112121213121412151216121712181219122012211222122312241225122612271228122912301231123212331234123512361237123812391240124112421243124412451246124712481249125012511252125312541255125612571258125912601261126212631264126512661267126812691270127112721273127412751276127712781279128012811282128312841285128612871288128912901291129212931294129512961297129812991300130113021303130413051306130713081309131013111312131313141315131613171318131913201321132213231324132513261327132813291330133113321333133413351336133713381339134013411342134313441345134613471348134913501351135213531354135513561357135813591360136113621363136413651366 |
- /***** spin: spinlex.c *****/
- /* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories. */
- /* All Rights Reserved. This software is for educational purposes only. */
- /* No guarantee whatsoever is expressed or implied by the distribution of */
- /* this code. Permission is given to distribute this code provided that */
- /* this introductory message is not removed and no monies are exchanged. */
- /* Software written by Gerard J. Holzmann. For tool documentation see: */
- /* http://spinroot.com/ */
- /* Send all bug-reports and/or questions to: bugs@spinroot.com */
- #include <stdlib.h>
- #include "spin.h"
- #ifdef PC
- #include "y_tab.h"
- #else
- #include "y.tab.h"
- #endif
- #define MAXINL 16 /* max recursion depth inline fcts */
- #define MAXPAR 32 /* max params to an inline call */
- #define MAXLEN 512 /* max len of an actual parameter text */
- typedef struct IType {
- Symbol *nm; /* name of the type */
- Lextok *cn; /* contents */
- Lextok *params; /* formal pars if any */
- char **anms; /* literal text for actual pars */
- char *prec; /* precondition for c_code or c_expr */
- int dln, cln; /* def and call linenr */
- Symbol *dfn, *cfn; /* def and call filename */
- struct IType *nxt; /* linked list */
- } IType;
- typedef struct C_Added {
- Symbol *s;
- Symbol *t;
- Symbol *ival;
- struct C_Added *nxt;
- } C_Added;
- extern RunList *X;
- extern ProcList *rdy;
- extern Symbol *Fname;
- extern Symbol *context, *owner;
- extern YYSTYPE yylval;
- extern short has_last, has_code;
- extern int verbose, IArgs, hastrack, separate;
- short has_stack = 0;
- int lineno = 1;
- char yytext[2048];
- FILE *yyin, *yyout;
- static C_Added *c_added, *c_tracked;
- static IType *Inline_stub[MAXINL];
- static char *ReDiRect;
- static char *Inliner[MAXINL], IArg_cont[MAXPAR][MAXLEN];
- static unsigned char in_comment=0;
- static int IArgno = 0, Inlining = -1;
- static int check_name(char *);
- #if 1
- #define Token(y) { if (in_comment) goto again; \
- yylval = nn(ZN,0,ZN,ZN); return y; }
- #define ValToken(x, y) { if (in_comment) goto again; \
- yylval = nn(ZN,0,ZN,ZN); yylval->val = x; return y; }
- #define SymToken(x, y) { if (in_comment) goto again; \
- yylval = nn(ZN,0,ZN,ZN); yylval->sym = x; return y; }
- #else
- #define Token(y) { yylval = nn(ZN,0,ZN,ZN); \
- if (!in_comment) return y; else goto again; }
- #define ValToken(x, y) { yylval = nn(ZN,0,ZN,ZN); yylval->val = x; \
- if (!in_comment) return y; else goto again; }
- #define SymToken(x, y) { yylval = nn(ZN,0,ZN,ZN); yylval->sym = x; \
- if (!in_comment) return y; else goto again; }
- #endif
- static int getinline(void);
- static void uninline(void);
- #if 1
- #define Getchar() ((Inlining<0)?getc(yyin):getinline())
- #define Ungetch(c) {if (Inlining<0) ungetc(c,yyin); else uninline(); }
- #else
- static int
- Getchar(void)
- { int c;
- if (Inlining<0)
- c = getc(yyin);
- else
- c = getinline();
- #if 1
- printf("<%c>", c);
- #endif
- return c;
- }
- static void
- Ungetch(int c)
- {
- if (Inlining<0)
- ungetc(c,yyin);
- else
- uninline();
- #if 1
- printf("<bs>");
- #endif
- }
- #endif
- static int
- notquote(int c)
- { return (c != '\"' && c != '\n');
- }
- int
- isalnum_(int c)
- { return (isalnum(c) || c == '_');
- }
- static int
- isalpha_(int c)
- { return isalpha(c); /* could be macro */
- }
-
- static int
- isdigit_(int c)
- { return isdigit(c); /* could be macro */
- }
- static void
- getword(int first, int (*tst)(int))
- { int i=0; char c;
- yytext[i++]= (char) first;
- while (tst(c = Getchar()))
- { yytext[i++] = c;
- if (c == '\\')
- yytext[i++] = Getchar(); /* no tst */
- }
- yytext[i] = '\0';
- Ungetch(c);
- }
- static int
- follow(int tok, int ifyes, int ifno)
- { int c;
- if ((c = Getchar()) == tok)
- return ifyes;
- Ungetch(c);
- return ifno;
- }
- static IType *seqnames;
- static void
- def_inline(Symbol *s, int ln, char *ptr, char *prc, Lextok *nms)
- { IType *tmp;
- char *nw = (char *) emalloc((int) strlen(ptr)+1);
- strcpy(nw, ptr);
- for (tmp = seqnames; tmp; tmp = tmp->nxt)
- if (!strcmp(s->name, tmp->nm->name))
- { non_fatal("procedure name %s redefined",
- tmp->nm->name);
- tmp->cn = (Lextok *) nw;
- tmp->params = nms;
- tmp->dln = ln;
- tmp->dfn = Fname;
- return;
- }
- tmp = (IType *) emalloc(sizeof(IType));
- tmp->nm = s;
- tmp->cn = (Lextok *) nw;
- tmp->params = nms;
- if (strlen(prc) > 0)
- { tmp->prec = (char *) emalloc((int) strlen(prc)+1);
- strcpy(tmp->prec, prc);
- }
- tmp->dln = ln;
- tmp->dfn = Fname;
- tmp->nxt = seqnames;
- seqnames = tmp;
- }
- void
- gencodetable(FILE *fd)
- { IType *tmp;
- char *q;
- int cnt;
- if (separate == 2) return;
- fprintf(fd, "struct {\n");
- fprintf(fd, " char *c; char *t;\n");
- fprintf(fd, "} code_lookup[] = {\n");
- if (has_code)
- for (tmp = seqnames; tmp; tmp = tmp->nxt)
- if (tmp->nm->type == CODE_FRAG
- || tmp->nm->type == CODE_DECL)
- { fprintf(fd, "\t{ \"%s\", ",
- tmp->nm->name);
- q = (char *) tmp->cn;
- while (*q == '\n' || *q == '\r' || *q == '\\')
- q++;
- fprintf(fd, "\"");
- cnt = 0;
- while (*q && cnt < 1024) /* pangen1.h allows 2048 */
- { switch (*q) {
- case '"':
- fprintf(fd, "\\\"");
- break;
- case '%':
- fprintf(fd, "%%");
- break;
- case '\n':
- fprintf(fd, "\\n");
- break;
- default:
- putc(*q, fd);
- break;
- }
- q++; cnt++;
- }
- if (*q) fprintf(fd, "...");
- fprintf(fd, "\"");
- fprintf(fd, " },\n");
- }
- fprintf(fd, " { (char *) 0, \"\" }\n");
- fprintf(fd, "};\n");
- }
- static int
- iseqname(char *t)
- { IType *tmp;
- for (tmp = seqnames; tmp; tmp = tmp->nxt)
- { if (!strcmp(t, tmp->nm->name))
- return 1;
- }
- return 0;
- }
- static int
- getinline(void)
- { int c;
- if (ReDiRect)
- { c = *ReDiRect++;
- if (c == '\0')
- { ReDiRect = (char *) 0;
- c = *Inliner[Inlining]++;
- }
- } else
- c = *Inliner[Inlining]++;
- if (c == '\0')
- { lineno = Inline_stub[Inlining]->cln;
- Fname = Inline_stub[Inlining]->cfn;
- Inlining--;
- #if 0
- if (verbose&32)
- printf("spin: line %d, done inlining %s\n",
- lineno, Inline_stub[Inlining+1]->nm->name);
- #endif
- return Getchar();
- }
- return c;
- }
- static void
- uninline(void)
- {
- if (ReDiRect)
- ReDiRect--;
- else
- Inliner[Inlining]--;
- }
- IType *
- find_inline(char *s)
- { IType *tmp;
- for (tmp = seqnames; tmp; tmp = tmp->nxt)
- if (!strcmp(s, tmp->nm->name))
- break;
- if (!tmp)
- fatal("cannot happen, missing inline def %s", s);
- return tmp;
- }
- void
- c_state(Symbol *s, Symbol *t, Symbol *ival) /* name, scope, ival */
- { C_Added *r;
- r = (C_Added *) emalloc(sizeof(C_Added));
- r->s = s; /* pointer to a data object */
- r->t = t; /* size of object, or "global", or "local proctype_name" */
- r->ival = ival;
- r->nxt = c_added;
- c_added = r;
- }
- void
- c_track(Symbol *s, Symbol *t, Symbol *stackonly) /* name, size */
- { C_Added *r;
- r = (C_Added *) emalloc(sizeof(C_Added));
- r->s = s;
- r->t = t;
- r->ival = stackonly; /* abuse of name */
- r->nxt = c_tracked;
- c_tracked = r;
- if (stackonly != ZS)
- { if (strcmp(stackonly->name, "\"Matched\"") == 0)
- r->ival = ZS; /* the default */
- else if (strcmp(stackonly->name, "\"UnMatched\"") != 0
- && strcmp(stackonly->name, "\"unMatched\"") != 0
- && strcmp(stackonly->name, "\"StackOnly\"") != 0)
- non_fatal("expecting '[Un]Matched', saw %s", stackonly->name);
- else
- has_stack = 1;
- }
- }
- char *
- jump_etc(char *op)
- { char *p = op;
- /* kludgy - try to get the type separated from the name */
- while (*p == ' ' || *p == '\t')
- p++; /* initial white space */
- while (*p != ' ' && *p != '\t')
- p++; /* type name */
- while (*p == ' ' || *p == '\t')
- p++; /* white space */
- while (*p == '*')
- p++; /* decorations */
- while (*p == ' ' || *p == '\t')
- p++; /* white space */
- if (*p == '\0')
- fatal("c_state format (%s)", op);
- if (strchr(p, '[')
- && !strchr(p, '{'))
- { non_fatal("array initialization error, c_state (%s)", p);
- return (char *) 0;
- }
- return p;
- }
- void
- c_add_globinit(FILE *fd)
- { C_Added *r;
- char *p, *q;
- fprintf(fd, "void\nglobinit(void)\n{\n");
- for (r = c_added; r; r = r->nxt)
- { if (r->ival == ZS)
- continue;
- if (strncmp(r->t->name, " Global ", strlen(" Global ")) == 0)
- { for (q = r->ival->name; *q; q++)
- { if (*q == '\"')
- *q = ' ';
- if (*q == '\\')
- *q++ = ' '; /* skip over the next */
- }
- p = jump_etc(r->s->name); /* e.g., "int **q" */
- if (p)
- fprintf(fd, " now.%s = %s;\n", p, r->ival->name);
- } else
- if (strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) == 0)
- { for (q = r->ival->name; *q; q++)
- { if (*q == '\"')
- *q = ' ';
- if (*q == '\\')
- *q++ = ' '; /* skip over the next */
- }
- p = jump_etc(r->s->name); /* e.g., "int **q" */
- if (p)
- fprintf(fd, " %s = %s;\n", p, r->ival->name); /* no now. prefix */
- } }
- fprintf(fd, "}\n");
- }
- void
- c_add_locinit(FILE *fd, int tpnr, char *pnm)
- { C_Added *r;
- char *p, *q, *s;
- int frst = 1;
- fprintf(fd, "void\nlocinit%d(int h)\n{\n", tpnr);
- for (r = c_added; r; r = r->nxt)
- if (r->ival != ZS
- && strncmp(r->t->name, " Local", strlen(" Local")) == 0)
- { for (q = r->ival->name; *q; q++)
- if (*q == '\"')
- *q = ' ';
-
- p = jump_etc(r->s->name); /* e.g., "int **q" */
- q = r->t->name + strlen(" Local");
- while (*q == ' ' || *q == '\t')
- q++; /* process name */
- s = (char *) emalloc(strlen(q)+1);
- strcpy(s, q);
- q = &s[strlen(s)-1];
- while (*q == ' ' || *q == '\t')
- *q-- = '\0';
- if (strcmp(pnm, s) != 0)
- continue;
- if (frst)
- { fprintf(fd, "\tuchar *this = pptr(h);\n");
- frst = 0;
- }
- if (p)
- fprintf(fd, " ((P%d *)this)->%s = %s;\n",
- tpnr, p, r->ival->name);
- }
- fprintf(fd, "}\n");
- }
- /* tracking:
- 1. for non-global and non-local c_state decls: add up all the sizes in c_added
- 2. add a global char array of that size into now
- 3. generate a routine that memcpy's the required values into that array
- 4. generate a call to that routine
- */
- void
- c_preview(void)
- { C_Added *r;
- hastrack = 0;
- if (c_tracked)
- hastrack = 1;
- else
- for (r = c_added; r; r = r->nxt)
- if (strncmp(r->t->name, " Global ", strlen(" Global ")) != 0
- && strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) != 0
- && strncmp(r->t->name, " Local", strlen(" Local")) != 0)
- { hastrack = 1; /* c_state variant now obsolete */
- break;
- }
- }
- int
- c_add_sv(FILE *fd) /* 1+2 -- called in pangen1.c */
- { C_Added *r;
- int cnt = 0;
- if (!c_added && !c_tracked) return 0;
- for (r = c_added; r; r = r->nxt) /* pickup global decls */
- if (strncmp(r->t->name, " Global ", strlen(" Global ")) == 0)
- fprintf(fd, " %s;\n", r->s->name);
- for (r = c_added; r; r = r->nxt)
- if (strncmp(r->t->name, " Global ", strlen(" Global ")) != 0
- && strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) != 0
- && strncmp(r->t->name, " Local", strlen(" Local")) != 0)
- { cnt++; /* obsolete use */
- }
- for (r = c_tracked; r; r = r->nxt)
- cnt++; /* preferred use */
- if (cnt == 0) return 0;
- cnt = 0;
- fprintf(fd, " uchar c_state[");
- for (r = c_added; r; r = r->nxt)
- if (strncmp(r->t->name, " Global ", strlen(" Global ")) != 0
- && strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) != 0
- && strncmp(r->t->name, " Local", strlen(" Local")) != 0)
- { fprintf(fd, "%ssizeof(%s)",
- (cnt==0)?"":"+", r->t->name);
- cnt++;
- }
- for (r = c_tracked; r; r = r->nxt)
- { if (r->ival != ZS) continue;
- fprintf(fd, "%s%s",
- (cnt==0)?"":"+", r->t->name);
- cnt++;
- }
- if (cnt == 0) fprintf(fd, "4"); /* now redundant */
- fprintf(fd, "];\n");
- return 1;
- }
- void
- c_add_stack(FILE *fd)
- { C_Added *r;
- int cnt = 0;
- if ((!c_added && !c_tracked) || !has_stack) return;
- for (r = c_tracked; r; r = r->nxt)
- if (r->ival != ZS)
- cnt++;
- if (cnt == 0) return;
- fprintf(fd, " uchar c_stack[");
- cnt = 0;
- for (r = c_tracked; r; r = r->nxt)
- { if (r->ival == ZS) continue;
- fprintf(fd, "%s%s",
- (cnt==0)?"":"+", r->t->name);
- cnt++;
- }
- if (cnt == 0) fprintf(fd, "4"); /* can't happen */
- fprintf(fd, "];\n");
- }
- void
- c_add_hidden(FILE *fd)
- { C_Added *r;
- for (r = c_added; r; r = r->nxt) /* pickup hidden decls */
- if (strncmp(r->t->name, "\"Hidden\"", strlen("\"Hidden\"")) == 0)
- { r->s->name[strlen(r->s->name)-1] = ' ';
- fprintf(fd, "%s; /* Hidden */\n", &r->s->name[1]);
- r->s->name[strlen(r->s->name)-1] = '"';
- }
- /* called before c_add_def - quotes are still there */
- }
- void
- c_add_loc(FILE *fd, char *s) /* state vector entries for proctype s */
- { C_Added *r;
- static char buf[1024];
- char *p;
- if (!c_added) return;
- strcpy(buf, s);
- strcat(buf, " ");
- for (r = c_added; r; r = r->nxt) /* pickup local decls */
- if (strncmp(r->t->name, " Local", strlen(" Local")) == 0)
- { p = r->t->name + strlen(" Local");
- while (*p == ' ' || *p == '\t')
- p++;
- if (strcmp(p, buf) == 0)
- fprintf(fd, " %s;\n", r->s->name);
- }
- }
- void
- c_add_def(FILE *fd) /* 3 - called in plunk_c_fcts() */
- { C_Added *r;
- fprintf(fd, "#if defined(C_States) && defined(HAS_TRACK)\n");
- for (r = c_added; r; r = r->nxt)
- { r->s->name[strlen(r->s->name)-1] = ' ';
- r->s->name[0] = ' '; /* remove the "s */
- r->t->name[strlen(r->t->name)-1] = ' ';
- r->t->name[0] = ' ';
- if (strncmp(r->t->name, " Global ", strlen(" Global ")) == 0
- || strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) == 0
- || strncmp(r->t->name, " Local", strlen(" Local")) == 0)
- continue;
- if (strchr(r->s->name, '&'))
- fatal("dereferencing state object: %s", r->s->name);
- fprintf(fd, "extern %s %s;\n", r->t->name, r->s->name);
- }
- for (r = c_tracked; r; r = r->nxt)
- { r->s->name[strlen(r->s->name)-1] = ' ';
- r->s->name[0] = ' '; /* remove " */
- r->t->name[strlen(r->t->name)-1] = ' ';
- r->t->name[0] = ' ';
- }
- if (separate == 2)
- { fprintf(fd, "#endif\n");
- return;
- }
- if (has_stack)
- { fprintf(fd, "void\nc_stack(char *p_t_r)\n{\n");
- fprintf(fd, "#ifdef VERBOSE\n");
- fprintf(fd, " printf(\"c_stack %%u\\n\", p_t_r);\n");
- fprintf(fd, "#endif\n");
- for (r = c_tracked; r; r = r->nxt)
- { if (r->ival == ZS) continue;
-
- fprintf(fd, "\tif(%s)\n", r->s->name);
- fprintf(fd, "\t\tmemcpy(p_t_r, %s, %s);\n",
- r->s->name, r->t->name);
- fprintf(fd, "\telse\n");
- fprintf(fd, "\t\tmemset(p_t_r, 0, %s);\n",
- r->t->name);
- fprintf(fd, "\tp_t_r += %s;\n", r->t->name);
- }
- fprintf(fd, "}\n\n");
- }
- fprintf(fd, "void\nc_update(char *p_t_r)\n{\n");
- fprintf(fd, "#ifdef VERBOSE\n");
- fprintf(fd, " printf(\"c_update %%u\\n\", p_t_r);\n");
- fprintf(fd, "#endif\n");
- for (r = c_added; r; r = r->nxt)
- { if (strncmp(r->t->name, " Global ", strlen(" Global ")) == 0
- || strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) == 0
- || strncmp(r->t->name, " Local", strlen(" Local")) == 0)
- continue;
- fprintf(fd, "\tmemcpy(p_t_r, &%s, sizeof(%s));\n",
- r->s->name, r->t->name);
- fprintf(fd, "\tp_t_r += sizeof(%s);\n", r->t->name);
- }
- for (r = c_tracked; r; r = r->nxt)
- { if (r->ival) continue;
- fprintf(fd, "\tif(%s)\n", r->s->name);
- fprintf(fd, "\t\tmemcpy(p_t_r, %s, %s);\n",
- r->s->name, r->t->name);
- fprintf(fd, "\telse\n");
- fprintf(fd, "\t\tmemset(p_t_r, 0, %s);\n",
- r->t->name);
- fprintf(fd, "\tp_t_r += %s;\n", r->t->name);
- }
- fprintf(fd, "}\n");
- if (has_stack)
- { fprintf(fd, "void\nc_unstack(char *p_t_r)\n{\n");
- fprintf(fd, "#ifdef VERBOSE\n");
- fprintf(fd, " printf(\"c_unstack %%u\\n\", p_t_r);\n");
- fprintf(fd, "#endif\n");
- for (r = c_tracked; r; r = r->nxt)
- { if (r->ival == ZS) continue;
- fprintf(fd, "\tif(%s)\n", r->s->name);
- fprintf(fd, "\t\tmemcpy(%s, p_t_r, %s);\n",
- r->s->name, r->t->name);
- fprintf(fd, "\tp_t_r += %s;\n", r->t->name);
- }
- fprintf(fd, "}\n");
- }
- fprintf(fd, "void\nc_revert(char *p_t_r)\n{\n");
- fprintf(fd, "#ifdef VERBOSE\n");
- fprintf(fd, " printf(\"c_revert %%u\\n\", p_t_r);\n");
- fprintf(fd, "#endif\n");
- for (r = c_added; r; r = r->nxt)
- { if (strncmp(r->t->name, " Global ", strlen(" Global ")) == 0
- || strncmp(r->t->name, " Hidden ", strlen(" Hidden ")) == 0
- || strncmp(r->t->name, " Local", strlen(" Local")) == 0)
- continue;
- fprintf(fd, "\tmemcpy(&%s, p_t_r, sizeof(%s));\n",
- r->s->name, r->t->name);
- fprintf(fd, "\tp_t_r += sizeof(%s);\n", r->t->name);
- }
- for (r = c_tracked; r; r = r->nxt)
- { if (r->ival != ZS) continue;
- fprintf(fd, "\tif(%s)\n", r->s->name);
- fprintf(fd, "\t\tmemcpy(%s, p_t_r, %s);\n",
- r->s->name, r->t->name);
- fprintf(fd, "\tp_t_r += %s;\n", r->t->name);
- }
- fprintf(fd, "}\n");
- fprintf(fd, "#endif\n");
- }
- void
- plunk_reverse(FILE *fd, IType *p, int matchthis)
- { char *y, *z;
- if (!p) return;
- plunk_reverse(fd, p->nxt, matchthis);
- if (!p->nm->context
- && p->nm->type == matchthis)
- { fprintf(fd, "\n/* start of %s */\n", p->nm->name);
- z = (char *) p->cn;
- while (*z == '\n' || *z == '\r' || *z == '\\')
- z++;
- /* e.g.: \#include "..." */
- y = z;
- while ((y = strstr(y, "\\#")) != NULL)
- { *y = '\n'; y++;
- }
- fprintf(fd, "%s\n", z);
- fprintf(fd, "\n/* end of %s */\n", p->nm->name);
- }
- }
- void
- plunk_c_decls(FILE *fd)
- {
- plunk_reverse(fd, seqnames, CODE_DECL);
- }
- void
- plunk_c_fcts(FILE *fd)
- {
- if (separate == 2 && hastrack)
- { c_add_def(fd);
- return;
- }
- c_add_hidden(fd);
- plunk_reverse(fd, seqnames, CODE_FRAG);
- if (c_added || c_tracked) /* enables calls to c_revert and c_update */
- fprintf(fd, "#define C_States 1\n");
- else
- fprintf(fd, "#undef C_States\n");
- if (hastrack)
- c_add_def(fd);
- c_add_globinit(fd);
- do_locinits(fd);
- }
- static void
- check_inline(IType *tmp)
- { char buf[128];
- ProcList *p;
- if (!X) return;
- for (p = rdy; p; p = p->nxt)
- { if (strcmp(p->n->name, X->n->name) == 0)
- continue;
- sprintf(buf, "P%s->", p->n->name);
- if (strstr((char *)tmp->cn, buf))
- { printf("spin: in proctype %s, ref to object in proctype %s\n",
- X->n->name, p->n->name);
- fatal("invalid variable ref in '%s'", tmp->nm->name);
- } }
- }
- void
- plunk_expr(FILE *fd, char *s)
- { IType *tmp;
- tmp = find_inline(s);
- check_inline(tmp);
- fprintf(fd, "%s", (char *) tmp->cn);
- }
- void
- preruse(FILE *fd, Lextok *n) /* check a condition for c_expr with preconditions */
- { IType *tmp;
- if (!n) return;
- if (n->ntyp == C_EXPR)
- { tmp = find_inline(n->sym->name);
- if (tmp->prec)
- { fprintf(fd, "if (!(%s)) { if (!readtrail) { depth++; ", tmp->prec);
- fprintf(fd, "trpt++; trpt->pr = II; trpt->o_t = t;");
- fprintf(fd, "trpt->st = tt; Uerror(\"%s\"); } ", tmp->prec);
- fprintf(fd, "else { printf(\"pan: precondition false: %s\\n\"); ", tmp->prec);
- fprintf(fd, "_m = 3; goto P999; } } \n\t\t");
- }
- } else
- { preruse(fd, n->rgt);
- preruse(fd, n->lft);
- }
- }
- int
- glob_inline(char *s)
- { IType *tmp;
- char *bdy;
- tmp = find_inline(s);
- bdy = (char *) tmp->cn;
- return (strstr(bdy, "now.") /* global ref or */
- || strchr(bdy, '(') > bdy); /* possible C-function call */
- }
- void
- plunk_inline(FILE *fd, char *s, int how) /* c_code with precondition */
- { IType *tmp;
- tmp = find_inline(s);
- check_inline(tmp);
- fprintf(fd, "{ ");
- if (how && tmp->prec)
- { fprintf(fd, "if (!(%s)) { if (!readtrail) { depth++; ", tmp->prec);
- fprintf(fd, "trpt++; trpt->pr = II; trpt->o_t = t;");
- fprintf(fd, "trpt->st = tt; Uerror(\"%s\"); } ", tmp->prec);
- fprintf(fd, "else { printf(\"pan: precondition false: %s\\n\"); ", tmp->prec);
- fprintf(fd, "_m = 3; goto P999; } } ");
- }
- fprintf(fd, "%s", (char *) tmp->cn);
- fprintf(fd, " }\n");
- }
- void
- no_side_effects(char *s)
- { IType *tmp;
- char *t;
- /* could still defeat this check via hidden
- * side effects in function calls,
- * but this will catch at least some cases
- */
- tmp = find_inline(s);
- t = (char *) tmp->cn;
- if (strchr(t, ';')
- || strstr(t, "++")
- || strstr(t, "--"))
- {
- bad: lineno = tmp->dln;
- Fname = tmp->dfn;
- non_fatal("c_expr %s has side-effects", s);
- return;
- }
- while ((t = strchr(t, '=')) != NULL)
- { if (*(t-1) == '!'
- || *(t-1) == '>'
- || *(t-1) == '<')
- { t++;
- continue;
- }
- t++;
- if (*t != '=')
- goto bad;
- t++;
- }
- }
- void
- pickup_inline(Symbol *t, Lextok *apars)
- { IType *tmp; Lextok *p, *q; int j;
- tmp = find_inline(t->name);
- if (++Inlining >= MAXINL)
- fatal("inline fcts too deeply nested", 0);
- tmp->cln = lineno; /* remember calling point */
- tmp->cfn = Fname; /* and filename */
- for (p = apars, q = tmp->params, j = 0; p && q; p = p->rgt, q = q->rgt)
- j++; /* count them */
- if (p || q)
- fatal("wrong nr of params on call of '%s'", t->name);
- tmp->anms = (char **) emalloc(j * sizeof(char *));
- for (p = apars, j = 0; p; p = p->rgt, j++)
- { tmp->anms[j] = (char *) emalloc((int) strlen(IArg_cont[j])+1);
- strcpy(tmp->anms[j], IArg_cont[j]);
- }
- lineno = tmp->dln; /* linenr of def */
- Fname = tmp->dfn; /* filename of same */
- Inliner[Inlining] = (char *)tmp->cn;
- Inline_stub[Inlining] = tmp;
- #if 0
- if (verbose&32)
- printf("spin: line %d, file %s, inlining '%s' (from line %d, file %s)\n",
- tmp->cln, tmp->cfn->name, t->name, tmp->dln, tmp->dfn->name);
- #endif
- for (j = 0; j < Inlining; j++)
- if (Inline_stub[j] == Inline_stub[Inlining])
- fatal("cyclic inline attempt on: %s", t->name);
- }
- static void
- do_directive(int first)
- { int c = first; /* handles lines starting with pound */
- getword(c, isalpha_);
- if (strcmp(yytext, "#ident") == 0)
- goto done;
- if ((c = Getchar()) != ' ')
- fatal("malformed preprocessor directive - # .", 0);
- if (!isdigit_(c = Getchar()))
- fatal("malformed preprocessor directive - # .lineno", 0);
- getword(c, isdigit_);
- lineno = atoi(yytext); /* pickup the line number */
- if ((c = Getchar()) == '\n')
- return; /* no filename */
- if (c != ' ')
- fatal("malformed preprocessor directive - .fname", 0);
- if ((c = Getchar()) != '\"')
- fatal("malformed preprocessor directive - .fname", 0);
- getword(c, notquote);
- if (Getchar() != '\"')
- fatal("malformed preprocessor directive - fname.", 0);
- strcat(yytext, "\"");
- Fname = lookup(yytext);
- done:
- while (Getchar() != '\n')
- ;
- }
- void
- precondition(char *q)
- { int c, nest = 1;
- for (;;)
- { c = Getchar();
- *q++ = c;
- switch (c) {
- case '\n':
- lineno++;
- break;
- case '[':
- nest++;
- break;
- case ']':
- if (--nest <= 0)
- { *--q = '\0';
- return;
- }
- break;
- }
- }
- fatal("cannot happen", (char *) 0);
- }
- Symbol *
- prep_inline(Symbol *s, Lextok *nms)
- { int c, nest = 1, dln, firstchar, cnr;
- char *p, buf[SOMETHINGBIG], buf2[RATHERSMALL];
- Lextok *t;
- static int c_code = 1;
- for (t = nms; t; t = t->rgt)
- if (t->lft)
- { if (t->lft->ntyp != NAME)
- fatal("bad param to inline %s", s->name);
- t->lft->sym->hidden |= 32;
- }
- if (!s) /* C_Code fragment */
- { s = (Symbol *) emalloc(sizeof(Symbol));
- s->name = (char *) emalloc((int) strlen("c_code")+26);
- sprintf(s->name, "c_code%d", c_code++);
- s->context = context;
- s->type = CODE_FRAG;
- } else
- s->type = PREDEF;
- p = &buf[0];
- buf2[0] = '\0';
- for (;;)
- { c = Getchar();
- switch (c) {
- case '[':
- if (s->type != CODE_FRAG)
- goto bad;
- precondition(&buf2[0]); /* e.g., c_code [p] { r = p-r; } */
- continue;
- case '{':
- break;
- case '\n':
- lineno++;
- /* fall through */
- case ' ': case '\t': case '\f': case '\r':
- continue;
- default :
- printf("spin: saw char '%c'\n", c);
- bad: fatal("bad inline: %s", s->name);
- }
- break;
- }
- dln = lineno;
- if (s->type == CODE_FRAG)
- { if (verbose&32)
- sprintf(buf, "\t/* line %d %s */\n\t\t",
- lineno, Fname->name);
- else
- strcpy(buf, "");
- } else
- sprintf(buf, "\n#line %d %s\n{", lineno, Fname->name);
- p += strlen(buf);
- firstchar = 1;
- cnr = 1; /* not zero */
- more:
- *p++ = c = Getchar();
- if (p - buf >= SOMETHINGBIG)
- fatal("inline text too long", 0);
- switch (c) {
- case '\n':
- lineno++;
- cnr = 0;
- break;
- case '{':
- cnr++;
- nest++;
- break;
- case '}':
- cnr++;
- if (--nest <= 0)
- { *p = '\0';
- if (s->type == CODE_FRAG)
- *--p = '\0'; /* remove trailing '}' */
- def_inline(s, dln, &buf[0], &buf2[0], nms);
- if (firstchar && s)
- printf("%3d: %s, warning: empty inline definition (%s)\n",
- dln, Fname->name, s->name);
- return s; /* normal return */
- }
- break;
- case '#':
- if (cnr == 0)
- { p--;
- do_directive(c); /* reads to newline */
- break;
- } /* else fall through */
- default:
- firstchar = 0;
- case '\t':
- case ' ':
- case '\f':
- cnr++;
- break;
- }
- goto more;
- }
- static int
- lex(void)
- { int c;
- again:
- c = Getchar();
- yytext[0] = (char) c;
- yytext[1] = '\0';
- switch (c) {
- case '\n': /* newline */
- lineno++;
- case '\r': /* carriage return */
- goto again;
- case ' ': case '\t': case '\f': /* white space */
- goto again;
- case '#': /* preprocessor directive */
- if (in_comment) goto again;
- do_directive(c);
- goto again;
- case '\"':
- getword(c, notquote);
- if (Getchar() != '\"')
- fatal("string not terminated", yytext);
- strcat(yytext, "\"");
- SymToken(lookup(yytext), STRING)
- case '\'': /* new 3.0.9 */
- c = Getchar();
- if (c == '\\')
- { c = Getchar();
- if (c == 'n') c = '\n';
- else if (c == 'r') c = '\r';
- else if (c == 't') c = '\t';
- else if (c == 'f') c = '\f';
- }
- if (Getchar() != '\'' && !in_comment)
- fatal("character quote missing: %s", yytext);
- ValToken(c, CONST)
- default:
- break;
- }
- if (isdigit_(c))
- { getword(c, isdigit_);
- ValToken(atoi(yytext), CONST)
- }
- if (isalpha_(c) || c == '_')
- { getword(c, isalnum_);
- if (!in_comment)
- { c = check_name(yytext);
- if (c) return c;
- /* else fall through */
- }
- goto again;
- }
- switch (c) {
- case '/': c = follow('*', 0, '/');
- if (!c) { in_comment = 1; goto again; }
- break;
- case '*': c = follow('/', 0, '*');
- if (!c) { in_comment = 0; goto again; }
- break;
- case ':': c = follow(':', SEP, ':'); break;
- case '-': c = follow('>', SEMI, follow('-', DECR, '-')); break;
- case '+': c = follow('+', INCR, '+'); break;
- case '<': c = follow('<', LSHIFT, follow('=', LE, LT)); break;
- case '>': c = follow('>', RSHIFT, follow('=', GE, GT)); break;
- case '=': c = follow('=', EQ, ASGN); break;
- case '!': c = follow('=', NE, follow('!', O_SND, SND)); break;
- case '?': c = follow('?', R_RCV, RCV); break;
- case '&': c = follow('&', AND, '&'); break;
- case '|': c = follow('|', OR, '|'); break;
- case ';': c = SEMI; break;
- default : break;
- }
- Token(c)
- }
- static struct {
- char *s; int tok; int val; char *sym;
- } Names[] = {
- {"active", ACTIVE, 0, 0},
- {"assert", ASSERT, 0, 0},
- {"atomic", ATOMIC, 0, 0},
- {"bit", TYPE, BIT, 0},
- {"bool", TYPE, BIT, 0},
- {"break", BREAK, 0, 0},
- {"byte", TYPE, BYTE, 0},
- {"c_code", C_CODE, 0, 0},
- {"c_decl", C_DECL, 0, 0},
- {"c_expr", C_EXPR, 0, 0},
- {"c_state", C_STATE, 0, 0},
- {"c_track", C_TRACK, 0, 0},
- {"D_proctype", D_PROCTYPE, 0, 0},
- {"do", DO, 0, 0},
- {"chan", TYPE, CHAN, 0},
- {"else", ELSE, 0, 0},
- {"empty", EMPTY, 0, 0},
- {"enabled", ENABLED, 0, 0},
- {"eval", EVAL, 0, 0},
- {"false", CONST, 0, 0},
- {"fi", FI, 0, 0},
- {"full", FULL, 0, 0},
- {"goto", GOTO, 0, 0},
- {"hidden", HIDDEN, 0, ":hide:"},
- {"if", IF, 0, 0},
- {"init", INIT, 0, ":init:"},
- {"int", TYPE, INT, 0},
- {"len", LEN, 0, 0},
- {"local", ISLOCAL, 0, ":local:"},
- {"mtype", TYPE, MTYPE, 0},
- {"nempty", NEMPTY, 0, 0},
- {"never", CLAIM, 0, ":never:"},
- {"nfull", NFULL, 0, 0},
- {"notrace", TRACE, 0, ":notrace:"},
- {"np_", NONPROGRESS, 0, 0},
- {"od", OD, 0, 0},
- {"of", OF, 0, 0},
- {"pc_value", PC_VAL, 0, 0},
- {"pid", TYPE, BYTE, 0},
- {"printf", PRINT, 0, 0},
- {"printm", PRINTM, 0, 0},
- {"priority", PRIORITY, 0, 0},
- {"proctype", PROCTYPE, 0, 0},
- {"provided", PROVIDED, 0, 0},
- {"run", RUN, 0, 0},
- {"d_step", D_STEP, 0, 0},
- {"inline", INLINE, 0, 0},
- {"short", TYPE, SHORT, 0},
- {"skip", CONST, 1, 0},
- {"timeout", TIMEOUT, 0, 0},
- {"trace", TRACE, 0, ":trace:"},
- {"true", CONST, 1, 0},
- {"show", SHOW, 0, ":show:"},
- {"typedef", TYPEDEF, 0, 0},
- {"unless", UNLESS, 0, 0},
- {"unsigned", TYPE, UNSIGNED, 0},
- {"xr", XU, XR, 0},
- {"xs", XU, XS, 0},
- {0, 0, 0, 0},
- };
- static int
- check_name(char *s)
- { int i;
- yylval = nn(ZN, 0, ZN, ZN);
- for (i = 0; Names[i].s; i++)
- if (strcmp(s, Names[i].s) == 0)
- { yylval->val = Names[i].val;
- if (Names[i].sym)
- yylval->sym = lookup(Names[i].sym);
- return Names[i].tok;
- }
- if ((yylval->val = ismtype(s)) != 0)
- { yylval->ismtyp = 1;
- return CONST;
- }
- if (strcmp(s, "_last") == 0)
- has_last++;
- if (Inlining >= 0 && !ReDiRect)
- { Lextok *tt, *t = Inline_stub[Inlining]->params;
- for (i = 0; t; t = t->rgt, i++) /* formal pars */
- if (!strcmp(s, t->lft->sym->name) /* varname matches formal */
- && strcmp(s, Inline_stub[Inlining]->anms[i]) != 0) /* actual pars */
- {
- #if 0
- if (verbose&32)
- printf("\tline %d, replace %s in call of '%s' with %s\n",
- lineno, s,
- Inline_stub[Inlining]->nm->name,
- Inline_stub[Inlining]->anms[i]);
- #endif
-
- for (tt = Inline_stub[Inlining]->params; tt; tt = tt->rgt)
- if (!strcmp(Inline_stub[Inlining]->anms[i],
- tt->lft->sym->name))
- { /* would be cyclic if not caught */
- printf("spin: line %d replacement value: %s\n",
- lineno, tt->lft->sym->name);
- fatal("formal par of %s matches replacement value",
- Inline_stub[Inlining]->nm->name);
- yylval->ntyp = tt->lft->ntyp;
- yylval->sym = lookup(tt->lft->sym->name);
- return NAME;
- }
- ReDiRect = Inline_stub[Inlining]->anms[i];
- return 0;
- } }
- yylval->sym = lookup(s); /* symbol table */
- if (isutype(s))
- return UNAME;
- if (isproctype(s))
- return PNAME;
- if (iseqname(s))
- return INAME;
- return NAME;
- }
- int
- yylex(void)
- { static int last = 0;
- static int hold = 0;
- int c;
- /*
- * repair two common syntax mistakes with
- * semi-colons before or after a '}'
- */
- if (hold)
- { c = hold;
- hold = 0;
- } else
- { c = lex();
- if (last == ELSE
- && c != SEMI
- && c != FI)
- { hold = c;
- last = 0;
- return SEMI;
- }
- if (last == '}'
- && c != PROCTYPE
- && c != INIT
- && c != CLAIM
- && c != SEP
- && c != FI
- && c != OD
- && c != '}'
- && c != UNLESS
- && c != SEMI
- && c != EOF)
- { hold = c;
- last = 0;
- return SEMI; /* insert ';' */
- }
- if (c == SEMI)
- { /* if context, we're not in a typedef
- * because they're global.
- * if owner, we're at the end of a ref
- * to a struct field -- prevent that the
- * lookahead is interpreted as a field of
- * the same struct...
- */
- if (context) owner = ZS;
- hold = lex(); /* look ahead */
- if (hold == '}'
- || hold == SEMI)
- { c = hold; /* omit ';' */
- hold = 0;
- }
- }
- }
- last = c;
- if (IArgs)
- { static int IArg_nst = 0;
- if (strcmp(yytext, ",") == 0)
- { IArg_cont[++IArgno][0] = '\0';
- } else if (strcmp(yytext, "(") == 0)
- { if (IArg_nst++ == 0)
- { IArgno = 0;
- IArg_cont[0][0] = '\0';
- } else
- strcat(IArg_cont[IArgno], yytext);
- } else if (strcmp(yytext, ")") == 0)
- { if (--IArg_nst > 0)
- strcat(IArg_cont[IArgno], yytext);
- } else if (c == CONST && yytext[0] == '\'')
- { sprintf(yytext, "'%c'", yylval->val);
- strcat(IArg_cont[IArgno], yytext);
- } else
- { strcat(IArg_cont[IArgno], yytext);
- }
- }
- return c;
- }
|