spinlex.c

这是一个同样来自贝尔实验室的和UNIX有着渊源的操作系统, 其简洁的设计和实现易于我们学习和理解

/***** 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: [e-mail]            */

#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