/***** 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: bugs@spinroot.com            *//* (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"#include <assert.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, old_scope_rules, nclaims;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, enum btypes);static void	tc_predef_np(void);static void	put_pinit(ProcList *);static void	multi_init(void);       void	walk_struct(FILE *, int, char *, Symbol *, char *, char *, char *); static voidreverse_names(ProcList *p){	if (!p) return;	reverse_names(p->nxt);	fprintf(th, "   \"%s\",\n", p->n->name);}static voidreverse_types(ProcList *p){	if (!p) return;	reverse_types(p->nxt);	fprintf(th, "   %d,	/* %s */\n", p->b, p->n->name);} static intblog(int n)	/* for small log2 without rounding problems */{	int m=1, r=2; 	while (r < n) { m++; r *= 2; }	return 1+m;} voidgenheader(void){	ProcList *p; int i; 	if (separate == 2)	{	putunames(th);		goto here;	}	/* 5.2.3: gcc 3 no longer seems to compute sizeof at compile time */	fprintf(th, "#define WS		%d /* word size in bytes */\n", (int) sizeof(void *));	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, "	#elif QUAD_CORE\n");	fprintf(th, "		#define NCORE	4\n");	fprintf(th, "	#else\n");	fprintf(th, "		#define NCORE	1\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_ */	if (nclaims > 1)	{	fprintf(tc, "\n#ifndef NOCLAIM\n");		fprintf(tc, "	, (short) Air%d", i+1);	/* Multi */		fprintf(tc, "\n#endif\n\t");	}	fprintf(tc, " };\n"); 	fprintf(th, "char *procname[] = {\n");		reverse_names(rdy);	fprintf(th, "   \":np_:\",\n");	fprintf(th, "};\n\n"); 	fprintf(th, "enum btypes { NONE=%d, N_CLAIM=%d,", NONE, N_CLAIM);	fprintf(th, " I_PROC=%d, A_PROC=%d,", I_PROC, A_PROC);	fprintf(th, " P_PROC=%d, E_TRACE=%d, N_TRACE=%d };\n",		P_PROC, E_TRACE, N_TRACE);	fprintf(th, "int Btypes[] = {\n");		reverse_types(rdy);	fprintf(th, "   0	/* :np_: */\n");	fprintf(th, "};\n\n"); here:	for (p = rdy; p; p = p->nxt)		put_ptype(p->n->name, p->tn, mst, nrRdy+1, p->b);		/* +1 for np_ */	put_ptype("np_", nrRdy, mst, nrRdy+1, 0); 	if (nclaims > 1)	{	/* this is the structure that goes into the state-vector		 * instead of the actual never claims		 * this assumes that the claims do not have any local variables		 * this claim records the types and states of all subclaims in an array		 * NB: not sure if we need the first 3 fields in this structure		 *     it's here for now to avoid breaking some possible dependence		 * in the calculations above, we were already taking into account		 * that there is one never-claim, which will now be this one		 */ 		i = blog(mst);		fprintf(th, "\n");		fprintf(th, "#ifndef NOCLAIM\n");		fprintf(th, "	#undef VERI\n");		fprintf(th, "	#define VERI	%d\n", nrRdy+1);		fprintf(th, "	#define Pclaim	P%d\n\n", nrRdy+1);		fprintf(th, "typedef struct P%d {\n", nrRdy+1);		fprintf(th, "	unsigned _pid : 8; /* always zero */\n");		fprintf(th, "	unsigned _t   : %d; /* active-claim type  */\n",			blog(nrRdy+1));		fprintf(th, "	unsigned _p   : %d; /* active-claim state */\n",			i);		fprintf(th, "	unsigned _n   : %d; /* active-claim index */\n",			blog(nclaims));		if (i <= 255)	/* in stdint.h = UCHAR_MAX from limits.h */		{	fprintf(th, "	uchar c_cur[NCLAIMS]; /* claim-states */\n");		} else if (i <= 65535)	/* really USHRT_MAX from limits.h */		{	fprintf(th, "	ushort c_cur[NCLAIMS]; /* claim-states */\n");		} else	/* the most unlikely case */		{	fprintf(th, "	uint c_cur[NCLAIMS]; /* claim-states */\n");		}		fprintf(th, "} P%d;\n", nrRdy+1);		fprintf(th, "uchar spin_c_typ[NCLAIMS]; /* claim-types */\n");		fprintf(th, "	#define Air%d	(0)\n\n", nrRdy+1);		fprintf(th, "#endif\n");		/*		 * find special states as:		 *	stopstate [ claimnr ][ curstate ] == 1		 *	accpstate [ claimnr ][ curstate ]		 *	progstate [ claimnr ][ curstate ]		 *	reached   [ claimnr ][ curstate ]		 *	visstate  [ claimnr ][ curstate ]		 *	loopstate [ claimnr ][ curstate ]		 *	mapstate  [ claimnr ][ curstate ]		 */	} else	{	fprintf(th, "\n#define Pclaim	P0\n");		fprintf(th, "#ifndef NCLAIMS\n");		fprintf(th, "	#define NCLAIMS 1\n");		fprintf(th, "#endif\n");		fprintf(th, "uchar spin_c_typ[NCLAIMS]; /* claim-types */\n");	} 	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, "#ifdef TRIX\n");	fprintf(th, "	/* room for 512 proc+chan ptrs, + safety margin */\n");	fprintf(th, "	char *_ids_[MAXPROC+MAXQ+4];\n");	fprintf(th, "#else\n");	fprintf(th, "	uchar sv[VECTORSZ];\n");	fprintf(th, "#endif\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, "#ifdef TRIX\n");	fprintf(th, "typedef struct TRIX_v6 {\n");	fprintf(th, "	uchar *body; /* aligned */\n");	fprintf(th, "#ifndef BFS\n");	fprintf(th, "	short modified;\n");	fprintf(th, "#endif\n");	fprintf(th, "	short psize;\n");	fprintf(th, "	short parent_pid;\n");	fprintf(th, "	struct TRIX_v6 *nxt;\n");	fprintf(th, "} TRIX_v6;\n");	fprintf(th, "TRIX_v6 *freebodies;\n");	fprintf(th, "TRIX_v6 *processes[MAXPROC+1];\n");	fprintf(th, "TRIX_v6 *channels[MAXQ+1]; \n");	fprintf(th, "long _p_count[MAXPROC];\n");	fprintf(th, "long _c_count[MAXPROC];\n");	fprintf(th, "#endif\n\n"); 	fprintf(th, "#define HAS_TRACK	%d\n", hastrack); 	if (separate != 2)		dohidden();} voidgenaddproc(void){	ProcList *p;	int i = 0, j; 	if (separate == 2) goto shortcut; 	fprintf(tc, "\n#ifdef TRIX\n");	fprintf(tc, "int what_p_size(int);\n");	fprintf(tc, "int what_q_size(int);\n\n");	/* the number of processes just changed by 1 (up or down) */	/* this means that the channel indices move up or down by one slot */	/* not all new channels may have a valid index yet, but we move */	/* all of them anyway, as if they existed */	fprintf(tc, "void\nre_mark_all(int whichway)\n");	fprintf(tc, "{	int j;\n");	fprintf(tc, "	#ifdef V_TRIX\n");	fprintf(tc, "		printf(\"%%d: re_mark_all channels %%d\\n\", depth, whichway);\n");	fprintf(tc, "	#endif\n");	fprintf(tc, "	#ifndef BFS\n");	fprintf(tc, "	for (j = 0; j < now._nr_qs; j++)\n");	fprintf(tc, "		channels[j]->modified = 1; /* channel index moved */\n");	fprintf(tc, "	#endif\n");	fprintf(tc, "	#ifndef TRIX_ORIG\n");	fprintf(tc, "	if (whichway > 0)\n");	fprintf(tc, "	{	for (j = now._nr_pr + now._nr_qs - 1; j >= now._nr_pr; j--)\n");	fprintf(tc, "			now._ids_[j] = now._ids_[j-1];\n");	fprintf(tc, "	} else\n");	fprintf(tc, "	{	for (j = now._nr_pr; j < now._nr_pr + now._nr_qs; j++)\n");	fprintf(tc, "			now._ids_[j] = now._ids_[j+1];\n");	fprintf(tc, "	}\n");	fprintf(tc, "	#endif\n");	fprintf(tc, "}\n"); 	fprintf(tc, "#endif\n\n"); 	fprintf(tc, "int\naddproc(int calling_pid, 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_ */ 	if (nclaims > 1)	{	fprintf(tc, "#ifndef NOCLAIM\n");		ntimes(tc, nrRdy+1, nrRdy+2, R5);		fprintf(tc, "#endif\n");	} 	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:	if (nclaims > 1)	{	multi_init();	}	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);} voiddo_locinits(FILE *fd){	ProcList *p; 	for (p = rdy; p; p = p->nxt)		c_add_locinit(fd, p->tn, p->n->name);} voidgenother(void){	ProcList *p; 	switch (separate) {	case 2:		if (nclaims > 0)		{	for (p = rdy; p; p = p->nxt)			{	if (p->b == N_CLAIM)				{	ntimes(tc, p->tn, p->tn+1, R0); /* claims only */		}	}	}		break;	case 1:		ntimes(tc,     0,    1, Code0);		for (p = rdy; p; p = p->nxt)		{	if (p->b != N_CLAIM)			{	ntimes(tc, p->tn, p->tn+1, R0); /* all except claims */		}	}		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 (nclaims > 0)		{	for (p = rdy; p; p = p->nxt)			{	if (p->b == N_CLAIM)				{	ntimes(tc, p->tn, p->tn+1, R0a); /* claims only */		}	}	}		return;	case 1:		for (p = rdy; p; p = p->nxt)		{	if (p->b != N_CLAIM)			{	ntimes(tc, p->tn, p->tn+1, R0a); /* all except claims */		}	}		fprintf(tc, "	if (state_tables)\n");		fprintf(tc, "		ini_claim(%d, 0);\n", claimnr);	/* the default claim */		if (acceptors == 0)		{	acceptors = 1;	/* assume at least 1 acceptstate */		}		break;	case 0:		ntimes(tc, 0, nrRdy, R0a);	/* all */		break;	} 	ntimes(th, acceptors,   acceptors+1,   Code1);	ntimes(th, progressors, progressors+1, Code3);	ntimes(th, nrRdy+1, nrRdy+2, R2); /* +1 for np_ */ 	ntimes(tc, 0,     1, Code2a);	/* dfs, bfs */	ntimes(tc, 0,     1, Code2c);	/* multicore */	ntimes(tc, 0,     1, Code2d); 	fprintf(tc, "void\ndo_reach(void)\n{\n");	ntimes(tc, 0,     nrRdy, R4);	fprintf(tc, "}\n\n"); 	fprintf(tc, "void\niniglobals(int calling_pid)\n{\n");	ntimes(tc, 1, u_sync+u_async+1, R3); /* because nqs is still 0 */	fprintf(tc, "\tMaxbody = max(Maxbody, sizeof(State)-VECTORSZ);\n");	fprintf(tc, "\tif ((Maxbody %% WS) != 0)\n");	fprintf(tc, "\t	Maxbody += WS - (Maxbody %% WS);\n\n"); 	/* after the value of Maxbody has settled */	if (doglobal("", INIV) > 0)	{	fprintf(tc, "#ifdef VAR_RANGES\n");		(void) doglobal("logval(\"", LOGV);		fprintf(tc, "#endif\n");	}	fprintf(tc, "}\n\n");} voidgensvmap(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 voidend_labs(Symbol *s, int i){	int oln = lineno;	Symbol *ofn = Fname;	Label *l;	int j; char foo[128]; 	if ((pid_is_claim(i) && separate == 1)	|| (!pid_is_claim(i) && 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;} voidntimes(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");	}} voidprehint(Symbol *s){	Lextok *n; 	printf("spin: warning, ");	if (!s) return; 	n = (s->context != ZS)?s->context->ini:s->ini;	if (n)	printf("line %s:%d, ", n->fn->name, n->ln);} voidchecktype(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;

Lines 1–500 of 1527. Load more