/***** 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    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; }#endifstatic 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(); }#elsestatic intGetchar(void){	int c;	if (Inlining<0)		c = getc(yyin);	else		c = getinline();#if 1	printf("<%c>", c);#endif	return c;}static voidUngetch(int c){	if (Inlining<0)		ungetc(c,yyin);	else		uninline();#if 1	printf("<bs>");#endif}#endifstatic intnotquote(int c){	return (c != '\"' && c != '\n');}intisalnum_(int c){	return (isalnum(c) || c == '_');}static intisalpha_(int c){	return isalpha(c);	/* could be macro */}       static intisdigit_(int c){	return isdigit(c);	/* could be macro */}static voidgetword(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 intfollow(int tok, int ifyes, int ifno){	int c;	if ((c = Getchar()) == tok)		return ifyes;	Ungetch(c);	return ifno;}static IType *seqnames;static voiddef_inline(Symbol *s, int ln, char *ptr, char *prc, Lextok *nms){	IType *tmp;	char *nw = (char *) emalloc(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(strlen(prc)+1);		strcpy(tmp->prec, prc);	}	tmp->dln = ln;	tmp->dfn = Fname;	tmp->nxt = seqnames;	seqnames = tmp;}voidgencodetable(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 intiseqname(char *t){	IType *tmp;	for (tmp = seqnames; tmp; tmp = tmp->nxt)	{	if (!strcmp(t, tmp->nm->name))			return 1;	}	return 0;}static intgetinline(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 voiduninline(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;}voidc_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;}voidc_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;}voidc_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");}voidc_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 */voidc_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 */