pangen1.c

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

/***** spin: pangen1.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 "spin.h"
#ifdef PC
#include "y_tab.h"
#else
#include "y.tab.h"
#endif
#include "pangen1.h"
#include "pangen3.h"

extern FILE	*tc, *th, *tt;
extern Label	*labtab;
extern Ordered	*all_names;
extern ProcList	*rdy;
extern Queue	*qtab;
extern Symbol	*Fname;
extern int	lineno, verbose, Pid, separate;
extern int	nrRdy, nqs, mst, Mpars, claimnr, eventmapnr;
extern short	has_sorted, has_random, has_provided;

int	Npars=0, u_sync=0, u_async=0, hastrack = 1;
short	has_io = 0;
short	has_state=0;	/* code contains c_state */

static Symbol	*LstSet=ZS;
static int	acceptors=0, progressors=0, nBits=0;
static int	Types[] = { UNSIGNED, BIT, BYTE, CHAN, MTYPE, SHORT, INT, STRUCT };

static int	doglobal(char *, int);
static void	dohidden(void);
static void	do_init(FILE *, Symbol *);
static void	end_labs(Symbol *, int);
static void	put_ptype(char *, int, int, int);
static void	tc_predef_np(void);
static void	put_pinit(ProcList *);
       void	walk_struct(FILE *, int, char *, Symbol *, char *, char *, char *);

static void
reverse_names(ProcList *p)
{
	if (!p) return;
	reverse_names(p->nxt);
	fprintf(th, "   \"%s\",\n", p->n->name);
}

void
genheader(void)
{	ProcList *p; int i;

	if (separate == 2)
	{	putunames(th);
		goto here;
	}

	fprintf(th, "#define SYNC	%d\n", u_sync);
	fprintf(th, "#define ASYNC	%d\n\n", u_async);

	putunames(th);

	fprintf(tc, "short Air[] = { ");
	for (p = rdy, i=0; p; p = p->nxt, i++)
		fprintf(tc, "%s (short) Air%d", (p!=rdy)?",":"", i);
	fprintf(tc, ", (short) Air%d", i);	/* np_ */
	fprintf(tc, " };\n");

	fprintf(th, "char *procname[] = {\n");
		reverse_names(rdy);
	fprintf(th, "   \":np_:\",\n");
	fprintf(th, "};\n\n");

here:
	for (p = rdy; p; p = p->nxt)
		put_ptype(p->n->name, p->tn, mst, nrRdy+1);
		/* +1 for np_ */
	put_ptype("np_", nrRdy, mst, nrRdy+1);

	ntimes(th, 0, 1, Head0);

	if (separate != 2)
	{	extern void c_add_stack(FILE *);

		ntimes(th, 0, 1, Header);
		c_add_stack(th);
		ntimes(th, 0, 1, Header0);
	}
	ntimes(th, 0, 1, Head1);

	LstSet = ZS;
	(void) doglobal("", PUTV);

	hastrack = c_add_sv(th);

	fprintf(th, "	uchar sv[VECTORSZ];\n");
	fprintf(th, "} State");
#ifdef SOLARIS
	fprintf(th,"\n#ifdef GCC\n");
	fprintf(th, "\t__attribute__ ((aligned(8)))");
	fprintf(th, "\n#endif\n\t");
#endif
	fprintf(th, ";\n\n");

	fprintf(th, "#define HAS_TRACK	%d\n", hastrack);

	if (separate != 2)
		dohidden();
}

void
genaddproc(void)
{	ProcList *p;
	int i = 0;

	if (separate ==2) goto shortcut;

	fprintf(tc, "int\naddproc(int n");
	for (i = 0; i < Npars; i++)
		fprintf(tc, ", int par%d", i);

	ntimes(tc, 0, 1, Addp0);
	ntimes(tc, 1, nrRdy+1, R5); /* +1 for np_ */
	ntimes(tc, 0, 1, Addp1);

	if (has_provided)
	{	fprintf(tt, "\nint\nprovided(int II, unsigned char ot, ");
		fprintf(tt, "int tt, Trans *t)\n");
		fprintf(tt, "{\n\tswitch(ot) {\n");
	}
shortcut:
	tc_predef_np();
	for (p = rdy; p; p = p->nxt)
	{	Pid = p->tn;
		put_pinit(p);
	}
	if (separate == 2) return;

	Pid = 0;
	if (has_provided)
	{	fprintf(tt, "\tdefault: return 1; /* e.g., a claim */\n");
		fprintf(tt, "\t}\n\treturn 0;\n}\n");
	}

	ntimes(tc, i, i+1, R6);
	if (separate == 0)
		ntimes(tc, 1, nrRdy+1, R5); /* +1 for np_ */
	else
		ntimes(tc, 1, nrRdy, R5);
	ntimes(tc, 0, 1, R8a);
}

void
do_locinits(FILE *fd)
{	ProcList *p;

	for (p = rdy; p; p = p->nxt)
		c_add_locinit(fd, p->tn, p->n->name);
}

void
genother(void)
{	ProcList *p;

	switch (separate) {
	case 2:
		if (claimnr >= 0)
		ntimes(tc, claimnr, claimnr+1, R0); /* claim only */
		break;
	case 1:
		ntimes(tc,     0,    1, Code0);
		ntimes(tc, 0, claimnr, R0);	/* all except claim */
		ntimes(tc, claimnr+1, nrRdy, R0);
		break;
	case 0:
		ntimes(tc,     0,    1, Code0);
		ntimes(tc,     0, nrRdy+1, R0); /* +1 for np_ */
		break;
	}

	for (p = rdy; p; p = p->nxt)
		end_labs(p->n, p->tn);

	switch (separate) {
	case 2:
		if (claimnr >= 0)
		ntimes(tc, claimnr, claimnr+1, R0a); /* claim only */
		return;
	case 1:
		ntimes(tc, 0, claimnr, R0a);	/* all except claim */
		ntimes(tc, claimnr+1, nrRdy, R0a);
		fprintf(tc, "	if (state_tables)\n");
		fprintf(tc, "		ini_claim(%d, 0);\n", claimnr);
		break;
	case 0:
		ntimes(tc, 0, nrRdy, R0a);	/* all */
		break;
	}

	ntimes(tc, 0,     1, R0b);
	if (separate == 1 && acceptors == 0)
		acceptors = 1;	/* assume at least 1 acceptstate */
	ntimes(th, acceptors,   acceptors+1,   Code1);
	ntimes(th, progressors, progressors+1, Code3);
	ntimes(th, nrRdy+1, nrRdy+2, R2); /* +1 for np_ */

	fprintf(tc, "	iniglobals();\n");
	ntimes(tc, 0,     1, Code2a);
	ntimes(tc, 0,     1, Code2b);	/* bfs option */
	ntimes(tc, 0,     1, Code2c);
	ntimes(tc, 0,     nrRdy, R4);
	fprintf(tc, "}\n\n");

	fprintf(tc, "void\n");
	fprintf(tc, "iniglobals(void)\n{\n");
	if (doglobal("", INIV) > 0)
	{	fprintf(tc, "#ifdef VAR_RANGES\n");
		(void) doglobal("logval(\"", LOGV);
		fprintf(tc, "#endif\n");
	}
	ntimes(tc, 1, nqs+1, R3);
	fprintf(tc, "\tMaxbody = max(Maxbody, sizeof(State)-VECTORSZ);");
	fprintf(tc, "\n}\n\n");
}

void
gensvmap(void)
{
	ntimes(tc, 0, 1, SvMap);
}

static struct {
	char *s,	*t;		int n,	m,	p;
} ln[] = {
	{"end",  	"stopstate",	3,	0,	0},
	{"progress",	"progstate",	8,	0,	1},
	{"accept",	"accpstate",	6,	1,	0},
	{0,		0,		0,	0,	0},
};

static void
end_labs(Symbol *s, int i)
{	int oln = lineno;
	Symbol *ofn = Fname;
	Label *l;
	int j; char foo[128];

	if ((i == claimnr && separate == 1)
	||  (i != claimnr && separate == 2))
		return;

	for (l = labtab; l; l = l->nxt)
	for (j = 0; ln[j].n; j++)
		if (strncmp(l->s->name, ln[j].s, ln[j].n) == 0
		&&  strcmp(l->c->name, s->name) == 0)
		{	fprintf(tc, "\t%s[%d][%d] = 1;\n",
				ln[j].t, i, l->e->seqno);
			acceptors += ln[j].m;
			progressors += ln[j].p;
			if (l->e->status & D_ATOM)
			{	sprintf(foo, "%s label inside d_step",
					ln[j].s);
				goto complain;
			}
			if (j > 0 && (l->e->status & ATOM))
			{	sprintf(foo, "%s label inside atomic",
					ln[j].s);
		complain:	lineno = l->e->n->ln;
				Fname  = l->e->n->fn;
				printf("spin: %3d:%s, warning, %s - is invisible\n",
					lineno, Fname?Fname->name:"-", foo);
			}
		}	
	/* visible states -- through remote refs: */
	for (l = labtab; l; l = l->nxt)
		if (l->visible
		&&  strcmp(l->s->context->name, s->name) == 0)
		fprintf(tc, "\tvisstate[%d][%d] = 1;\n",
				i, l->e->seqno);

	lineno = oln;
	Fname  = ofn;
}

void
ntimes(FILE *fd, int n, int m, char *c[])
{
	int i, j;
	for (j = 0; c[j]; j++)
	for (i = n; i < m; i++)
	{	fprintf(fd, c[j], i, i, i, i, i, i);
		fprintf(fd, "\n");
	}
}

void
prehint(Symbol *s)
{	Lextok *n;

	printf("spin: warning, ");
	if (!s) return;

	n = (s->context != ZS)?s->context->ini:s->ini;
	if (n)
	printf("line %3d %s, ", n->ln, n->fn->name);
}

void
checktype(Symbol *sp, char *s)
{	char buf[128]; int i;

	if (!s
	|| (sp->type != BYTE
	&&  sp->type != SHORT
	&&  sp->type != INT))
		return;

	if (sp->hidden&16)	/* formal parameter */
	{	ProcList *p; Lextok *f, *t;
		int posnr = 0;
		for (p = rdy; p; p = p->nxt)
			if (p->n->name
			&&  strcmp(s, p->n->name) == 0)
				break;
		if (p)
		for (f = p->p; f; f = f->rgt) /* list of types */
		for (t = f->lft; t; t = t->rgt, posnr++)
			if (t->sym
			&&  strcmp(t->sym->name, sp->name) == 0)
			{	checkrun(sp, posnr);
				return;
			}

	} else if (!(sp->hidden&4))
	{	if (!(verbose&32)) return;
		sputtype(buf, sp->type);
		i = (int) strlen(buf);
		while (buf[--i] == ' ') buf[i] = '\0';
		prehint(sp);
		if (sp->context)
			printf("proctype %s:", s);
		else
			printf("global");
		printf(" '%s %s' could be declared 'bit %s'\n",
			buf, sp->name, sp->name);
	} else if (sp->type != BYTE && !(sp->hidden&8))
	{	if (!(verbose&32)) return;
		sputtype(buf, sp->type);
		i = (int) strlen(buf);
		while (buf[--i] == ' ') buf[i] = '\0';
		prehint(sp);
		if (sp->context)
			printf("proctype %s:", s);
		else
			printf("global");
		printf(" '%s %s' could be declared 'byte %s'\n",
			buf, sp->name, sp->name);
	}
}

int
dolocal(FILE *ofd, char *pre, int dowhat, int p, char *s)
{	int h, j, k=0; extern int nr_errs;
	Ordered *walk;
	Symbol *sp;
	char buf[64], buf2[128], buf3[128];

	for (j = 0; j < 8; j++)
	for (h = 0; h <= 1; h++)
	for (walk = all_names; walk; walk = walk->next)
	{	sp = walk->entry;
		if (sp->context
		&& !sp->owner
		&&  sp->type == Types[j]
		&&  ((h == 0 && sp->nel == 1) || (h == 1 && sp->nel > 1))
		&&  strcmp(s, sp->context->name) == 0)
		{	switch (dowhat) {
			case LOGV:
				if (sp->type == CHAN
				&&  verbose == 0)
					break;
				sprintf(buf, "%s%s:", pre, s);
				{ sprintf(buf2, "\", ((P%d *)pptr(h))->", p);
				  sprintf(buf3, ");\n");
				}
				do_var(ofd, dowhat, "", sp, buf, buf2, buf3);
				break;
			case INIV:
				checktype(sp, s); /* fall through */
				if (sp->hidden&16) { k++; break; }
			case PUTV:
				sprintf(buf, "((P%d *)pptr(h))->", p);
				do_var(ofd, dowhat, buf, sp, "", " = ", ";\n");
				k++;
				break;
			}
			if (strcmp(s, ":never:") == 0)
			{	printf("error: %s defines local %s\n",
					s, sp->name);
				nr_errs++;
	}	}	}
	return k;
}

void
c_chandump(FILE *fd)
{	Queue *q;
	char buf[256];
	int i;

	if (!qtab)
	{	fprintf(fd, "void\nc_chandump(int unused) ");
		fprintf(fd, "{ unused = unused++; /* avoid complaints */ }\n");
		return;
	}

	fprintf(fd, "void\nc_chandump(int from)\n");
	fprintf(fd, "{	uchar *z; int slot;\n");

	fprintf(fd, "	from--;\n");
	fprintf(fd, "	if (from >= (int) now._nr_qs || from < 0)\n");
	fprintf(fd, "	{	printf(\"pan: bad qid %%d\\n\", from+1);\n");
	fprintf(fd, "		return;\n");
	fprintf(fd, "	}\n");
	fprintf(fd, "	z = qptr(from);\n");
	fprintf(fd, "	switch (((Q0 *)z)->_t) {\n");

	for (q = qtab; q; q = q->nxt)
	{	fprintf(fd, "	case %d:\n\t\t", q->qid);
		sprintf(buf, "((Q%d *)z)->", q->qid);

		fprintf(fd, "for (slot = 0; slot < %sQlen; slot++)\n\t\t", buf);
		fprintf(fd, "{	printf(\" [\");\n\t\t");
		for (i = 0; i < q->nflds; i++)
		{	if (q->fld_width[i] == MTYPE)
			{	fprintf(fd, "\tprintm(%scontents[slot].fld%d);\n\t\t",
				buf, i);
			} else
			fprintf(fd, "\tprintf(\"%%d,\", %scontents[slot].fld%d);\n\t\t",
				buf, i);
		}
		fprintf(fd, "	printf(\"],\");\n\t\t");
		fprintf(fd, "}\n\t\t");
		fprintf(fd, "break;\n");
	}
	fprintf(fd, "	}\n");
	fprintf(fd, "	printf(\"\\n\");\n}\n");
}

void
c_var(FILE *fd, char *pref, Symbol *sp)
{	char buf[256];
	int i;

	switch (sp->type) {
	case STRUCT:
		/* c_struct(fd, pref, sp); */
		fprintf(fd, "\t\tprintf(\"\t(struct %s)\\n\");\n",
			sp->name);
		sprintf(buf, "%s%s.", pref, sp->name);
		c_struct(fd, buf, sp);
		break;
	case BIT:   case BYTE:
	case SHORT: case INT:
	case UNSIGNED:
		sputtype(buf, sp->type);
		if (sp->nel == 1)
		fprintf(fd, "\tprintf(\"\t%s %s:\t%%d\\n\", %s%s);\n",
			buf, sp->name, pref, sp->name);
		else
		for (i = 0; i < sp->nel; i++)
		fprintf(fd, "\tprintf(\"\t%s %s[%d]:\t%%d\\n\", %s%s[%d]);\n",
			buf, sp->name, i, pref, sp->name, i);
		break;
	case CHAN:
		if (sp->nel == 1)
		{  fprintf(fd, "\tprintf(\"\tchan %s (=%%d):\tlen %%d:\\t\", ",
			sp->name);
		   fprintf(fd, "%s%s, q_len(%s%s));\n",
			pref, sp->name, pref, sp->name);
		   fprintf(fd, "\tc_chandump(%s%s);\n", pref, sp->name);
		} else
		for (i = 0; i < sp->nel; i++)
		{  fprintf(fd, "\tprintf(\"\tchan %s[%d] (=%%d):\tlen %%d:\\t\", ",
			sp->name, i);
		   fprintf(fd, "%s%s[%d], q_len(%s%s[%d]));\n",
			pref, sp->name, i, pref, sp->name, i);
		   fprintf(fd, "\tc_chandump(%s%s[%d]);\n",
			pref, sp->name, i);
		}
		break;
	}
}

void
c_splurge(FILE *fd, ProcList *p)
{	Ordered *walk;
	Symbol *sp;
	char pref[64];

	if (strcmp(p->n->name, ":never:") != 0
	&&  strcmp(p->n->name, ":trace:") != 0
	&&  strcmp(p->n->name, ":notrace:") != 0)
	for (walk = all_names; walk; walk = walk->next)
	{	sp = walk->entry;
		if (!sp->context
		||  strcmp(sp->context->name, p->n->name) != 0
		||  sp->owner || (sp->hidden&1)
		|| (sp->type == MTYPE && ismtype(sp->name)))
			continue;

		sprintf(pref, "((P%d *)pptr(pid))->", p->tn);
		c_var(fd, pref, sp);
	}
}

void
c_wrapper(FILE *fd)	/* allow pan.c to print out global sv entries */
{	Ordered *walk;
	ProcList *p;
	Symbol *sp;
	Lextok *n;
	extern Lextok *Mtype;
	int j;

	fprintf(fd, "void\nc_globals(void)\n{\t/* int i; */\n");
	fprintf(fd, "	printf(\"global vars:\\n\");\n");
	for (walk = all_names; walk; walk = walk->next)
	{	sp = walk->entry;
		if (sp->context || sp->owner || (sp->hidden&1)
		|| (sp->type == MTYPE && ismtype(sp->name)))
			continue;

		c_var(fd, "now.", sp);
	}
	fprintf(fd, "}\n");

	fprintf(fd, "void\nc_locals(int pid, int tp)\n{\t/* int i; */\n");
	fprintf(fd, "	switch(tp) {\n");
	for (p = rdy; p; p = p->nxt)
	{	fprintf(fd, "	case %d:\n", p->tn);
		fprintf(fd, "	\tprintf(\"local vars proc %%d (%s):\\n\", pid);\n",
			p->n->name);
		c_splurge(fd, p);
		fprintf(fd, "	\tbreak;\n");
	}
	fprintf(fd, "	}\n}\n");

	fprintf(fd, "void\nprintm(int x)\n{\n");
	fprintf(fd, "	switch (x) {\n");
        for (n = Mtype, j = 1; n && j; n = n->rgt, j++)
                fprintf(fd, "\tcase %d: Printf(\"%s\"); break;\n",
			j, n->lft->sym->name);
	fprintf(fd, "	default: Printf(\"%%d\", x);\n");
	fprintf(fd, "	}\n");
	fprintf(fd, "}\n");
}

static int
doglobal(char *pre, int dowhat)
{	Ordered *walk;
	Symbol *sp;
	int j, cnt = 0;

	for (j = 0; j < 8; j++)
	for (walk = all_names; walk; walk = walk->next)
	{	sp = walk->entry;
		if (!sp->context
		&&  !sp->owner
		&&  sp->type == Types[j])
		{	if (Types[j] != MTYPE || !ismtype(sp->name))
			switch (dowhat) {
			case LOGV:
				if (sp->type == CHAN
				&&  verbose == 0)
					break;
				if (sp->hidden&1)
					break;
				do_var(tc, dowhat, "", sp,
					pre, "\", now.", ");\n");
				break;
			case INIV:
				checktype(sp, (char *) 0);
				cnt++; /* fall through */
			case PUTV:
				do_var(tc, dowhat, (sp->hidden&1)?"":"now.", sp,
				"", " = ", ";\n");
				break;
	}	}	}
	return cnt;
}

static void
dohidden(void)
{	Ordered *walk;
	Symbol *sp;
	int j;

	for (j = 0; j < 8; j++)
	for (walk = all_names; walk; walk = walk->next)
	{	sp = walk->entry;
		if ((sp->hidden&1)