/***** 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 intGetchar(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 voidUngetch(int c){	if (Inlining<0)		ungetc(c,yyin);	else		uninline();	if (0)	{	printf("<bs>");	}}#endif static intnotdollar(int c){	return (c != '$' && c != '\n');} static 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;	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;} 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: %s:%d, done inlining %s\n",			Fname, lineno, Inline_stub[Inlining+1]->nm->name);#endif		return Getchar();	}	return c;} static voiduninline(void){	if (ReDiRect)		ReDiRect--;	else		Inliner[Inlining]--;} intis_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;} 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 */			break;		}} intc_add_sv(FILE *fd)	/* 1+2 -- called in pangen1.c */{	C_Added *r;	int cnt = 0; 	if (!c_added && !c_tracked) return 0; 

Lines 1–500 of 1521. Load more