pangen1.c

对软件进行可达性测试的软件

/***** 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]            */
/* (c) 2007: small additions for V5.0 to support multi-core verifications */

#include "spin.h"
#include "y.tab.h"
#include "pangen1.h"
#include "pangen3.h"
#include "pangen6.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;
extern Queue	*ltab[];

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);
	fprintf(th, "#ifndef NCORE\n");
	fprintf(th, "	#ifdef DUAL_CORE\n");
	fprintf(th, "		#define NCORE	2\n");
	fprintf(th, "	#else\n");
	fprintf(th, "		#define NCORE	1	/* by default use 1 cpu */\n");
	fprintf(th, "	#endif\n");
	fprintf(th, "#endif\n");

	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 *);
		extern void c_stack_size(FILE *);

		ntimes(th, 0, 1, Header);
		fprintf(th, "#define StackSize	(");
			c_stack_size(th);
		fprintf(th, ")\n");

		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,     1, Code2d);
	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 (i > 0 && 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];

	if (dowhat == INIV)
	{	/* initialize in order of declaration */
		for (walk = all_names; walk; walk = walk->next)
		{	sp = walk->entry;
			if (sp->context
			&& !sp->owner
			&&  strcmp(s, sp->context->name) == 0)
			{	checktype(sp, s); /* fall through */
				if (!(sp->hidden&16))
				{	sprintf(buf, "((P%d *)pptr(h))->", p);
					do_var(ofd, dowhat, buf, sp, "", " = ", ";\n");
				}
				k++;
		}	}
	} else
	{	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 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++;
	}	}	}	}