Rev 2 | Blame | Compare with Previous | Last modification | View Log | RSS feed
/***** 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"
#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 */
char **anms; /* literal text for actual pars */
char *prec; /* precondition for c_code or c_expr */
int uiid; /* unique inline id */
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, *oFname;
extern Symbol *context, *owner;
extern YYSTYPE yylval;
extern short has_last, has_code;
extern int verbose, IArgs, hastrack, separate, ltl_mode;
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 *);
#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 (0)
{ printf("<%c:%d>[%d] ", c, c, Inlining);
} else
{ printf("%c", c);
}
return c;
}
static void
Ungetch(int c)
{
if (Inlining<0)
ungetc(c,yyin);
else
uninline();
if (0)
{ printf("<bs>");
}
}
#endif
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;
}
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->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; /* unmatched stack */
}
}
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_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");
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, "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 %%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(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 %%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\"); continue; } ", 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, 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(\"%s\"); continue; ",
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");
}
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("inlines nested too deeply", 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(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);
}
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;
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
lex(void)
{ int c;
again:
c = Getchar();
yytext[0] = (char) c;
yytext[1] = '\0';
switch (c) {
case EOF:
return 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 '$':
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))
{ 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;
}
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('>', 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;
case '.': c = follow('.', DOTDOT, '.'); break;
case '{': scope_seq[scope_level++]++; set_cur_scope(); break;
case '}': scope_level--; set_cur_scope(); break;
default : break;
}
Token(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},
{"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},
{"run", RUN, 0, 0},
{"d_step", D_STEP, 0, 0},
{"select", SELECT, 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);
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: %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;
} 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 if (c == CONST)
{ sprintf(yytext, "%d", yylval->val);
strcat(IArg_cont[IArgno], yytext);
} else
{
switch (c) {
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;
}
strcat(IArg_cont[IArgno], yytext);
}
}
return c;
}