* This file is part of the public release of Spin. It is subject to the

/***** spin: spinlex.c *****/

/*
* This file is part of the public release of Spin. It is subject to the
* terms in the LICENSE file that is included in this source directory.
* Tool documentation is available at http://spinroot.com
*/

#include <stdlib.h>
#include <assert.h>
#include <errno.h>
#include <ctype.h>
#include "spin.h"
#include "y.tab.h"

#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 */
Lextok *rval; /* variable to assign return value, if any */
char **anms; /* literal text for actual pars */
char *prec; /* precondition for c_code or c_expr */
int uiid; /* unique inline id */
int is_expr; /* c_expr in an ltl formula */
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;
Symbol *fnm;
int lno;
struct C_Added *nxt;
} C_Added;

extern RunList *X;
extern ProcList *rdy;
extern Symbol *Fname, *oFname;
extern Symbol *context, *owner;
extern YYSTYPE yylval;
extern short has_last, has_code, has_priority;
extern int verbose, IArgs, hastrack, separate, in_for;
extern int implied_semis, ltl_mode, in_seq, par_cnt;

short has_stack = 0;
int lineno = 1;
int scope_seq[128], scope_level = 0;
char CurScope[MAXSCOPESZ];
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 *);
static int last_token = 0;

#define ValToken(x, y) { if (in_comment) goto again; \
yylval = nn(ZN,0,ZN,ZN); \
yylval->val = x; \
last_token = y; \
return y; \
}

#define SymToken(x, y) { if (in_comment) goto again; \
yylval = nn(ZN,0,ZN,ZN); \
yylval->sym = x; \
last_token = y; \
return y; \
}

static int getinline(void);
static void uninline(void);

static int PushBack;
static int PushedBack;
static char pushedback[4096];

static void
push_back(char *s)
{
if (PushedBack + strlen(s) > 4094)
{ fatal("select statement too large", 0);
}
strcat(pushedback, s);
PushedBack += strlen(s);
}

static int
Getchar(void)
{ int c;

if (PushedBack > 0 && PushBack < PushedBack)
{ c = pushedback[PushBack++];
if (PushBack == PushedBack)
{ pushedback[0] = '\0';
PushBack = PushedBack = 0;
}
return c; /* expanded select statement */
}
if (Inlining<0)
{ c = getc(yyin);
} else
{ c = getinline();
}
#if 0
if (0)
{ printf("<%c:%d>[%d] ", c, c, Inlining);
} else
{ printf("%c", c);
}
#endif
return c;
}

static void
Ungetch(int c)
{
if (PushedBack > 0 && PushBack > 0)
{ PushBack--;
return;
}

if (Inlining<0)
{ ungetc(c,yyin);
} else
{ uninline();
}
if (0)
{ printf("\n<bs{%d}bs>\n", c);
}
}

static int
notdollar(int c)
{ return (c != '$' && c != '\n');
}

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, c;

yytext[i++]= (char) first;
while (tst(c = Getchar()))
{ yytext[i++] = (char) c;
if (c == '\\')
{ c = Getchar();
yytext[i++] = (char) c; /* 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;
int cnt = 0;
char *nw = (char *) emalloc(strlen(ptr)+1);
strcpy(nw, ptr);

for (tmp = seqnames; tmp; cnt++, 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(strlen(prc)+1);
strcpy(tmp->prec, prc);
}
tmp->dln = ln;
tmp->dfn = Fname;
tmp->uiid = cnt+1; /* so that 0 means: not an inline */
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;
}

Lextok *
return_statement(Lextok *n)
{
if (Inline_stub[Inlining]->rval)
{ Lextok *g = nn(ZN, NAME, ZN, ZN);
Lextok *h = Inline_stub[Inlining]->rval;
g->sym = lookup("rv_");
return nn(h, ASGN, h, n);
} else
{ fatal("return statement outside inline", (char *) 0);
}
return ZN;
}

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: %s:%d, done inlining %s\n",
Fname, lineno, Inline_stub[Inlining+1]->nm->name);
#endif
return Getchar();
}
return c;
}

static void
uninline(void)
{
if (ReDiRect)
ReDiRect--;
else
Inliner[Inlining]--;
}

int
is_inline(void)
{
if (Inlining < 0)
return 0; /* i.e., not an inline */
if (Inline_stub[Inlining] == NULL)
fatal("unexpected, inline_stub not set", 0);
return Inline_stub[Inlining]->uiid;
}

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->lno = lineno;
r->fnm = Fname;
r->nxt = c_added;

if(strncmp(r->s->name, "\"unsigned unsigned", 18) == 0)
{ int i;
for (i = 10; i < 18; i++)
{ r->s->name[i] = ' ';
}
/* printf("corrected <%s>\n", r->s->name); */
}
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;
r->fnm = Fname;
r->lno = lineno;
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; /* unmatched stack */
}
}

char *
skip_white(char *p)
{
if (p != NULL)
{ while (*p == ' ' || *p == '\t')
p++;
} else
{ fatal("bad format - 1", (char *) 0);
}
return p;
}

char *
skip_nonwhite(char *p)
{
if (p != NULL)
{ while (*p != ' ' && *p != '\t')
p++;
} else
{ fatal("bad format - 2", (char *) 0);
}
return p;
}

static char *
jump_etc(C_Added *r)
{ char *op = r->s->name;
char *p = op;
char *q = (char *) 0;
int oln = lineno;
Symbol *ofnm = Fname;

/* try to get the type separated from the name */
lineno = r->lno;
Fname = r->fnm;

p = skip_white(p); /* initial white space */

if (strncmp(p, "enum", strlen("enum")) == 0) /* special case: a two-part typename */
{ p += strlen("enum")+1;
p = skip_white(p);
}
if (strncmp(p, "unsigned", strlen("unsigned")) == 0) /* possibly a two-part typename */
{ p += strlen("unsigned")+1;
q = p = skip_white(p);
}
p = skip_nonwhite(p); /* type name */
p = skip_white(p); /* white space */
while (*p == '*') p++; /* decorations */
p = skip_white(p); /* white space */

if (*p == '\0')
{ if (q)
{ p = q; /* unsigned with implied 'int' */
} else
{ fatal("c_state format (%s)", op);
} }

if (strchr(p, '[') && !strchr(p, '{'))
{ non_fatal("array initialization error, c_state (%s)", p);
p = (char *) 0;
}

lineno = oln;
Fname = ofnm;

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); /* 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); /* 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); /* 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, "\t\t((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_stack_size(FILE *fd)
{ C_Added *r;
int cnt = 0;

for (r = c_tracked; r; r = r->nxt)
if (r->ival != ZS)
{ fprintf(fd, "%s%s",
(cnt==0)?"":"+", r->t->name);
cnt++;
}
if (cnt == 0)
{ fprintf(fd, "WS");
}
}

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)
{ fprintf(fd, " uchar c_stack[StackSize];\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");
fprintf(fd, "/* XXX p=<%s>, s=<%s>, buf=<%s> r->s->name=<%s>XXX */\n", p, s, buf, r->s->name);
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) && (HAS_TRACK==1)\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, "int cpu_printf(const char *, ...);\n");
fprintf(fd, "void\nc_stack(uchar *p_t_r)\n{\n");
fprintf(fd, "#ifdef VERBOSE\n");
fprintf(fd, " cpu_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(uchar *p_t_r)\n{\n");
fprintf(fd, "#ifdef VERBOSE\n");
fprintf(fd, " printf(\"c_update %%p\\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(uchar *p_t_r)\n{\n");
fprintf(fd, "#ifdef VERBOSE\n");
fprintf(fd, " cpu_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(uchar *p_t_r)\n{\n");
fprintf(fd, "#ifdef VERBOSE\n");
fprintf(fd, " printf(\"c_revert %%p\\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
&& p->is_expr == 0)
{ 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);
} }
}

extern short terse;
extern short nocast;

void
plunk_expr(FILE *fd, char *s)
{ IType *tmp;
char *q;

tmp = find_inline(s);
check_inline(tmp);

if (terse && nocast)
{ for (q = (char *) tmp->cn; q && *q != '\0'; q++)
{ fflush(fd);
if (*q == '"')
{ fprintf(fd, "\\");
}
fprintf(fd, "%c", *q);
}
} else
{ 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; trpt->st = tt; ");
fprintf(fd, "uerror(\"c_expr line %d precondition false: %s\"); continue;",
tmp->dln, 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 */
}

char *
put_inline(FILE *fd, char *s)
{ IType *tmp;

tmp = find_inline(s);
check_inline(tmp);
return (char *) tmp->cn;
}

void
mark_last(void)
{
if (seqnames)
{ seqnames->is_expr = 1;
}
}

void
plunk_inline(FILE *fd, char *s, int how, int gencode) /* 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) {",
tmp->prec);
fprintf(fd, " uerror(\"c_code line %d precondition false: %s\"); continue; ",
tmp->dln,
tmp->prec);
fprintf(fd, "} else { ");
fprintf(fd, "printf(\"pan: precondition false: %s\\n\"); _m = 3; goto P999; } } ",
tmp->prec);
}

if (!gencode) /* not in d_step */
{ fprintf(fd, "\n\t\tsv_save();");
}

fprintf(fd, "%s", (char *) tmp->cn);
fprintf(fd, " }\n");
}

int
side_scan(char *t, char *pat)
{ char *r = strstr(t, pat);
return (r
&& *(r-1) != '"'
&& *(r-1) != '\'');
}

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 (side_scan(t, ";")
|| side_scan(t, "++")
|| side_scan(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-1) == '"'
|| *(t-1) == '\'')
{ t += 2;
continue;
}
t++;
if (*t != '=')
goto bad;
t++;
}
}

void
pickup_inline(Symbol *t, Lextok *apars, Lextok *rval)
{ IType *tmp; Lextok *p, *q; int j;

tmp = find_inline(t->name);

if (++Inlining >= MAXINL)
fatal("inlines nested too deeply", 0);
tmp->cln = lineno; /* remember calling point */
tmp->cfn = Fname; /* and filename */
tmp->rval = rval;

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(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: %s:%d, inlining '%s' (from %s:%d)\n",
tmp->cfn->name, tmp->cln, t->name, tmp->dfn->name, tmp->dln);
#endif
for (j = 0; j < Inlining; j++)
{ if (Inline_stub[j] == Inline_stub[Inlining])
{ fatal("cyclic inline attempt on: %s", t->name);
} }
last_token = SEMI; /* avoid insertion of extra semi */
}

extern int pp_mode;

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()) != '\"')
{ printf("got %c, expected \" -- lineno %d\n", c, lineno);
fatal("malformed preprocessor directive - .fname (%s)", yytext);
}

getword(Getchar(), notquote); /* was 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); /* unreachable */
}

Symbol *
prep_inline(Symbol *s, Lextok *nms)
{ int c, nest = 1, dln, firstchar, cnr;
char *p;
Lextok *t;
static char Buf1[SOMETHINGBIG], Buf2[RATHERSMALL];
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?s->name:"--");
t->lft->sym->hidden |= 32;
}

if (!s) /* C_Code fragment */
{ s = (Symbol *) emalloc(sizeof(Symbol));
s->name = (char *) emalloc(strlen("c_code")+26);
sprintf(s->name, "c_code%d", c_code++);
s->context = context;
s->type = CODE_FRAG;
} else
{ s->type = PREDEF;
}

p = &Buf1[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(Buf1, "\t/* line %d %s */\n\t\t",
lineno, Fname->name);
} else
{ strcpy(Buf1, "");
}
} else
{ sprintf(Buf1, "\n#line %d \"%s\"\n{", lineno, Fname->name);
}
p += strlen(Buf1);
firstchar = 1;

cnr = 1; /* not zero */
more:
c = Getchar();
*p++ = (char) c;
if (p - Buf1 >= 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, &Buf1[0], &Buf2[0], nms);
if (firstchar)
{ 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 */
} else
{ firstchar = 0;
cnr++;
}
break;
case '\t':
case ' ':
case '\f':
cnr++;
break;
case '"':
do {
c = Getchar();
*p++ = (char) c;
if (c == '\\')
{ *p++ = (char) Getchar();
}
if (p - Buf1 >= SOMETHINGBIG)
{ fatal("inline text too long", 0);
}
} while (c != '"'); /* end of string */
/* *p = '\0'; */
break;
case '\'':
c = Getchar();
*p++ = (char) c;
if (c == '\\')
{ *p++ = (char) Getchar();
}
c = Getchar();
*p++ = (char) c;
assert(c == '\'');
break;
default:
firstchar = 0;
cnr++;
break;
}
goto more;
}

static void
set_cur_scope(void)
{ int i;
char tmpbuf[256];

strcpy(CurScope, "_");

if (context)
for (i = 0; i < scope_level; i++)
{ sprintf(tmpbuf, "%d_", scope_seq[i]);
strcat(CurScope, tmpbuf);
}
}

static int
pre_proc(void)
{ char b[512];
int c, i = 0;

b[i++] = '#';
while ((c = Getchar()) != '\n' && c != EOF)
{ b[i++] = (char) c;
}
b[i] = '\0';
yylval = nn(ZN, 0, ZN, ZN);
yylval->sym = lookup(b);
return PREPROC;
}

static int specials[] = {
'}', ')', ']',
OD, FI, ELSE, BREAK,
C_CODE, C_EXPR, C_DECL,
NAME, CONST, INCR, DECR, 0
};

int
follows_token(int c)
{ int i;

for (i = 0; specials[i]; i++)
{ if (c == specials[i])
{ return 1;
} }
return 0;
}
#define DEFER_LTL
#ifdef DEFER_LTL
/* defer ltl formula to the end of the spec
* no matter where they appear in the original
*/

static int deferred = 0;
static FILE *defer_fd;

int
get_deferred(void)
{
if (!defer_fd)
{ return 0; /* nothing was deferred */
}
fclose(defer_fd);

defer_fd = fopen(TMP_FILE2, "r");
if (!defer_fd)
{ non_fatal("cannot retrieve deferred ltl formula", (char *) 0);
return 0;
}
fclose(yyin);
yyin = defer_fd;
return 1;
}

void
zap_deferred(void)
{
(void) unlink(TMP_FILE2);
}

int
put_deferred(void)
{ int c, cnt;
if (!defer_fd)
{ defer_fd = fopen(TMP_FILE2, "w+");
if (!defer_fd)
{ non_fatal("cannot defer ltl expansion", (char *) 0);
return 0;
} }
fprintf(defer_fd, "ltl ");
cnt = 0;
while ((c = getc(yyin)) != EOF)
{ if (c == '{')
{ cnt++;
}
if (c == '}')
{ cnt--;
if (cnt == 0)
{ break;
} }
fprintf(defer_fd, "%c", c);
}
fprintf(defer_fd, "}\n");
fflush(defer_fd);
return 1;
}
#endif

#define EXPAND_SELECT
#ifdef EXPAND_SELECT
static char tmp_hold[256];
static int tmp_has;

void
new_select(void)
{ tmp_hold[0] = '\0';
tmp_has = 0;
}

int
scan_to(int stop, int (*tst)(int), char *buf)
{ int c, i = 0;

do { c = Getchar();
if (tmp_has < sizeof(tmp_hold))
{ tmp_hold[tmp_has++] = c;
}
if (c == '\n')
{ lineno++;
} else if (buf)
{ buf[i++] = c;
}
if (tst && !tst(c) && c != ' ' && c != '\t')
{ break;
}
} while (c != stop && c != EOF);

if (buf)
{ buf[i-1] = '\0';
}

if (c != stop)
{ if (0)
{ printf("saw: '%c', expected '%c'\n", c, stop);
}
if (tmp_has < sizeof(tmp_hold))
{ tmp_hold[tmp_has] = '\0';
push_back(tmp_hold);
if (0)
{ printf("pushed back: <'%s'>\n", tmp_hold);
}
return 0; /* internal expansion fails */
} else
{ fatal("expecting select ( name : constant .. constant )", 0);
} }
return 1; /* success */
}
#endif

int
lex(void)
{ int c;
again:
c = Getchar();
yytext[0] = (char) c;
yytext[1] = '\0';
switch (c) {
case EOF:
#ifdef DEFER_LTL
if (!deferred)
{ deferred = 1;
if (get_deferred())
{ goto again;
}
} else
{ zap_deferred();
}
#endif
return c;
case '\n': /* newline */
lineno++;
/* make most semi-colons optional */
if (implied_semis
/* && context */
&& in_seq
&& par_cnt == 0
&& follows_token(last_token))
{ if (0)
{ printf("insert ; line %d, last_token %d in_seq %d\n",
lineno-1, last_token, in_seq);
}
ValToken(1, SEMI);
}
/* else fall thru */
case '\r': /* carriage return */
goto again;

case ' ': case '\t': case '\f': /* white space */
goto again;

case '#': /* preprocessor directive */
if (in_comment) goto again;
if (pp_mode)
{ last_token = PREPROC;
return pre_proc();
}
do_directive(c);
goto again;

case '\"':
getword(c, notquote);
if (Getchar() != '\"')
fatal("string not terminated", yytext);
strcat(yytext, "\"");
SymToken(lookup(yytext), STRING)

case '$':
getword('\"', notdollar);
if (Getchar() != '$')
fatal("ltl definition 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))
{ long int nr;
getword(c, isdigit_);
errno = 0;
nr = strtol(yytext, NULL, 10);
if (errno != 0)
{ fprintf(stderr, "spin: value out of range: '%s' read as '%d'\n",
yytext, (int) nr);
}
ValToken((int)nr, CONST)
}

if (isalpha_(c) || c == '_')
{ getword(c, isalnum_);
if (!in_comment)
{ c = check_name(yytext);

#ifdef EXPAND_SELECT
if (c == SELECT && Inlining < 0)
{ char name[64], from[32], upto[32];
int i, a, b;
new_select();
if (!scan_to('(', 0, 0)
|| !scan_to(':', isalnum, name)
|| !scan_to('.', isdigit, from)
|| !scan_to('.', 0, 0)
|| !scan_to(')', isdigit, upto))
{ goto not_expanded;
}
a = atoi(from);
b = atoi(upto);
if (0)
{ printf("Select %s from %d to %d\n",
name, a, b);
}
if (a > b)
{ non_fatal("bad range in select statement", 0);
goto again;
}
if (b - a <= 32)
{ push_back("if ");
for (i = a; i <= b; i++)
{ char buf[128];
push_back(":: ");
sprintf(buf, "%s = %d ",
name, i);
push_back(buf);
}
push_back("fi ");
} else
{ char buf[128];
sprintf(buf, "%s = %d; do ",
name, a);
push_back(buf);
sprintf(buf, ":: (%s < %d) -> %s++ ",
name, b, name);
push_back(buf);
push_back(":: break od; ");
}
goto again;
}
not_expanded:
#endif

#ifdef DEFER_LTL
if (c == LTL && !deferred)
{ if (put_deferred())
{ goto again;
} }
#endif
if (c)
{ last_token = c;
return c;
}
/* else fall through */
}
goto again;
}

if (ltl_mode)
{ switch (c) {
case '-': c = follow('>', IMPLIES, '-'); break;
case '[': c = follow(']', ALWAYS, '['); break;
case '<': c = follow('>', EVENTUALLY, '<');
if (c == '<')
{ c = Getchar();
if (c == '-')
{ c = follow('>', EQUIV, '-');
if (c == '-')
{ Ungetch(c);
c = '<';
}
} else
{ Ungetch(c);
c = '<';
} }
default: break;
} }

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('>', ARROW, 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;
case '.': c = follow('.', DOTDOT, '.'); break;
case '{': scope_seq[scope_level++]++; set_cur_scope(); break;
case '}': scope_level--; set_cur_scope(); break;
default : break;
}
ValToken(0, c)
}

static struct {
char *s; int tok;
} LTL_syms[] = {
/* [], <>, ->, and <-> are intercepted in lex() */
{ "U", UNTIL },
{ "V", RELEASE },
{ "W", WEAK_UNTIL },
{ "X", NEXT },
{ "always", ALWAYS },
{ "eventually", EVENTUALLY },
{ "until", UNTIL },
{ "stronguntil",UNTIL },
{ "weakuntil", WEAK_UNTIL },
{ "release", RELEASE },
{ "next", NEXT },
{ "implies", IMPLIES },
{ "equivalent", EQUIV },
{ 0, 0 },
};

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},
{"for", FOR, 0, 0},
{"full", FULL, 0, 0},
{"get_priority", GET_P, 0, 0},
{"goto", GOTO, 0, 0},
{"hidden", HIDDEN, 0, ":hide:"},
{"if", IF, 0, 0},
{"in", IN, 0, 0},
{"init", INIT, 0, ":init:"},
{"inline", INLINE, 0, 0},
{"int", TYPE, INT, 0},
{"len", LEN, 0, 0},
{"local", ISLOCAL, 0, ":local:"},
{"ltl", LTL, 0, ":ltl:"},
{"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},
{"return", RETURN, 0, 0},
{"run", RUN, 0, 0},
{"d_step", D_STEP, 0, 0},
{"select", SELECT, 0, 0},
{"set_priority", SET_P, 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);

if (ltl_mode)
{ for (i = 0; LTL_syms[i].s; i++)
{ if (strcmp(s, LTL_syms[i].s) == 0)
{ return LTL_syms[i].tok;
} } }

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);
if (Names[i].tok == IN && !in_for)
{ continue;
}
return Names[i].tok;
} }

if ((yylval->val = ismtype(s)) != 0)
{ yylval->ismtyp = 1;
return CONST;
}

if (strcmp(s, "_last") == 0)
has_last++;

if (strcmp(s, "_priority") == 0)
has_priority++;

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: %s:%d replacement value: %s\n",
oFname->name?oFname->name:"--", lineno, tt->lft->sym->name);
fatal("formal par of %s contains replacement value",
Inline_stub[Inlining]->nm->name);
yylval->ntyp = tt->lft->ntyp;
yylval->sym = lookup(tt->lft->sym->name);
return NAME;
}

/* check for occurrence of param as field of struct */
{ char *ptr = Inline_stub[Inlining]->anms[i];
while ((ptr = strstr(ptr, s)) != NULL)
{ if (*(ptr-1) == '.'
|| *(ptr+strlen(s)) == '.')
{ fatal("formal par of %s used in structure name",
Inline_stub[Inlining]->nm->name);
}
ptr++;
} }
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;
last_token = c;
} else
{ c = lex();
if (last == ELSE
&& c != SEMI
&& c != ARROW
&& c != FI)
{ hold = c;
last = 0;
last_token = SEMI;
return SEMI;
}
if (last == '}'
&& c != PROCTYPE
&& c != INIT
&& c != CLAIM
&& c != SEP
&& c != FI
&& c != OD
&& c != '}'
&& c != UNLESS
&& c != SEMI
&& c != ARROW
&& c != EOF)
{ hold = c;
last = 0;
last_token = SEMI;
return SEMI; /* insert ';' */
}
if (c == SEMI || c == ARROW)
{ /* 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 == ARROW
|| 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
{ assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont));
strcat(IArg_cont[IArgno], yytext);
}
} else if (strcmp(yytext, ")") == 0)
{ if (--IArg_nst > 0)
{ assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont));
strcat(IArg_cont[IArgno], yytext);
}
} else if (c == CONST && yytext[0] == '\'')
{ sprintf(yytext, "'%c'", yylval->val);
assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont));
strcat(IArg_cont[IArgno], yytext);
} else if (c == CONST)
{ sprintf(yytext, "%d", yylval->val);
assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont));
strcat(IArg_cont[IArgno], yytext);
} else
{
switch (c) {
case ARROW: strcpy(yytext, "->"); break; /* NEW */
case SEP: strcpy(yytext, "::"); break;
case SEMI: strcpy(yytext, ";"); break;
case DECR: strcpy(yytext, "--"); break;
case INCR: strcpy(yytext, "++"); break;
case LSHIFT: strcpy(yytext, "<<"); break;
case RSHIFT: strcpy(yytext, ">>"); break;
case LE: strcpy(yytext, "<="); break;
case LT: strcpy(yytext, "<"); break;
case GE: strcpy(yytext, ">="); break;
case GT: strcpy(yytext, ">"); break;
case EQ: strcpy(yytext, "=="); break;
case ASGN: strcpy(yytext, "="); break;
case NE: strcpy(yytext, "!="); break;
case R_RCV: strcpy(yytext, "??"); break;
case RCV: strcpy(yytext, "?"); break;
case O_SND: strcpy(yytext, "!!"); break;
case SND: strcpy(yytext, "!"); break;
case AND: strcpy(yytext, "&&"); break;
case OR: strcpy(yytext, "||"); break;
}
assert(strlen(IArg_cont[IArgno])+strlen(yytext) < sizeof(IArg_cont));
strcat(IArg_cont[IArgno], yytext);
}
}
return c;
}