pangen2.c

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

/***** spin: pangen2.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 "version.h"
#include "y.tab.h"
#include "pangen2.h"
#include "pangen4.h"
#include "pangen5.h"

#define DELTA	500	/* sets an upperbound on nr of chan names */

#define blurb(fd, e)	{ fprintf(fd, "\n"); if (!merger) fprintf(fd, "\t\t/* %s:%d */\n", \
				e->n->fn->name, e->n->ln); }
#define tr_map(m, e)	{ if (!merger) fprintf(tt, "\t\ttr_2_src(%d, %s, %d);\n", \
				m, e->n->fn->name, e->n->ln); }

extern ProcList	*rdy;
extern RunList	*run;
extern Symbol	*Fname, *oFname, *context;
extern char	*claimproc, *eventmap;
extern int	lineno, verbose, Npars, Mpars;
extern int	m_loss, has_remote, has_remvar, merger, rvopt, separate;
extern int	Ntimeouts, Etimeouts, deadvar;
extern int	u_sync, u_async, nrRdy, Unique;
extern int	GenCode, IsGuard, Level, TestOnly;
extern short	has_stack;
extern char	*NextLab[];

FILE	*tc, *th, *tt, *tb;
static FILE	*tm;

int	OkBreak = -1, has_hidden = 0; /* has_hidden set in sym.c and structs.c */
short	nocast=0;	/* to turn off casts in lvalues */
short	terse=0;	/* terse printing of varnames */
short	no_arrays=0;
short	has_last=0;	/* spec refers to _last */
short	has_badelse=0;	/* spec contains else combined with chan refs */
short	has_enabled=0;	/* spec contains enabled() */
short	has_pcvalue=0;	/* spec contains pc_value() */
short	has_np=0;	/* spec contains np_ */
short	has_sorted=0;	/* spec contains `!!' (sorted-send) operator */
short	has_random=0;	/* spec contains `??' (random-recv) operator */
short	has_xu=0;	/* spec contains xr or xs assertions */
short	has_unless=0;	/* spec contains unless statements */
short	has_provided=0;	/* spec contains PROVIDED clauses on procs */
short	has_code=0;	/* spec contains c_code, c_expr, c_state */
short	evalindex=0;	/* evaluate index of var names */
int	mst=0;		/* max nr of state/process */
int	claimnr = -1;	/* claim process, if any */
int	eventmapnr = -1; /* event trace, if any */
int	Pid;		/* proc currently processed */
int	multi_oval;	/* set in merges, used also in pangen4.c */

#define MAXMERGE	256	/* max nr of bups per merge sequence */

static short	CnT[MAXMERGE];
static Lextok	XZ, YZ[MAXMERGE];
static int	didcase, YZmax, YZcnt;

static Lextok	*Nn[2];
static int	Det;	/* set if deterministic */
static int	T_sum, T_mus, t_cyc;
static int	TPE[2], EPT[2];
static int	uniq=1;
static int	multi_needed, multi_undo;
static short	AllGlobal=0;	/* set if process has provided clause */
static short	withprocname=0;	/* prefix local varnames with procname */
static short	_isok=0;	/* checks usage of predefined variable _ */

int	has_global(Lextok *);
static int	getweight(Lextok *);
static int	scan_seq(Sequence *);
static void	genconditionals(void);
static void	mark_seq(Sequence *);
static void	patch_atomic(Sequence *);
static void	put_seq(Sequence *, int, int);
static void	putproc(ProcList *);
static void	Tpe(Lextok *);
extern void	spit_recvs(FILE *, FILE*);

static int
fproc(char *s)
{	ProcList *p;

	for (p = rdy; p; p = p->nxt)
		if (strcmp(p->n->name, s) == 0)
			return p->tn;

	fatal("proctype %s not found", s);
	return -1;
}

static void
reverse_procs(RunList *q)
{
	if (!q) return;
	reverse_procs(q->nxt);
	fprintf(tc, "	Addproc(%d);\n", q->tn);
}

static void
tm_predef_np(void)
{
	fprintf(th, "#define _T5	%d\n", uniq++);
	fprintf(th, "#define _T2	%d\n", uniq++);

	if (Unique < (1 << (8*sizeof(unsigned char)) ))	/* was uniq before */
	{	fprintf(th, "#define T_ID	unsigned char\n");
	} else if (Unique < (1 << (8*sizeof(unsigned short)) ))
	{	fprintf(th, "#define T_ID	unsigned short\n");
	} else
	{	fprintf(th, "#define T_ID	unsigned int\n");
	}

	fprintf(tm, "\tcase  _T5:\t/* np_ */\n");

	if (separate == 2)
	fprintf(tm, "\t\tif (!((!(o_pm&4) && !(tau&128))))\n");
	else
	fprintf(tm, "\t\tif (!((!(trpt->o_pm&4) && !(trpt->tau&128))))\n");

	fprintf(tm, "\t\t\tcontinue;\n");
	fprintf(tm, "\t\t/* else fall through */\n");
	fprintf(tm, "\tcase  _T2:\t/* true */\n");
	fprintf(tm, "\t\t_m = 3; goto P999;\n");
}

static void
tt_predef_np(void)
{
	fprintf(tt, "\t/* np_ demon: */\n");
	fprintf(tt, "\ttrans[_NP_] = ");
	fprintf(tt, "(Trans **) emalloc(2*sizeof(Trans *));\n");
	fprintf(tt, "\tT = trans[_NP_][0] = ");
	fprintf(tt, "settr(9997,0,1,_T5,0,\"(np_)\", 1,2,0);\n");
	fprintf(tt, "\t    T->nxt	  = ");
	fprintf(tt, "settr(9998,0,0,_T2,0,\"(1)\",   0,2,0);\n");
	fprintf(tt, "\tT = trans[_NP_][1] = ");
	fprintf(tt, "settr(9999,0,1,_T5,0,\"(np_)\", 1,2,0);\n");
}

static struct {
	char *nm[3];
} Cfile[] = {
	{ { "pan.c", "pan_s.c", "pan_t.c" } },
	{ { "pan.h", "pan_s.h", "pan_t.h" } },
	{ { "pan.t", "pan_s.t", "pan_t.t" } },
	{ { "pan.m", "pan_s.m", "pan_t.m" } },
	{ { "pan.b", "pan_s.b", "pan_t.b" } }
};

void
gensrc(void)
{	ProcList *p;

	if (!(tc = fopen(Cfile[0].nm[separate], "w"))		/* main routines */
	||  !(th = fopen(Cfile[1].nm[separate], "w"))		/* header file   */
	||  !(tt = fopen(Cfile[2].nm[separate], "w"))		/* transition matrix */
	||  !(tm = fopen(Cfile[3].nm[separate], "w"))		/* forward  moves */
	||  !(tb = fopen(Cfile[4].nm[separate], "w")))	/* backward moves */
	{	printf("spin: cannot create pan.[chtmfb]\n");
		alldone(1);
	}

	fprintf(th, "#define SpinVersion	\"%s\"\n", SpinVersion);
	fprintf(th, "#define PanSource	\"%s\"\n\n", oFname->name);

	fprintf(th, "#ifdef WIN64\n");
	fprintf(th, "#define ONE_L	((unsigned long) 1)\n");
	fprintf(th, "#define long	long long\n");
	fprintf(th, "#else\n");
	fprintf(th, "#define ONE_L	(1L)\n");
	fprintf(th, "#endif\n");

	if (separate != 2)
	fprintf(th, "char *TrailFile = PanSource; /* default */\n");

	fprintf(th, "#if defined(BFS)\n");
	fprintf(th, "#ifndef SAFETY\n");
	fprintf(th, "#define SAFETY\n");
	fprintf(th, "#endif\n");
	fprintf(th, "#ifndef XUSAFE\n");
	fprintf(th, "#define XUSAFE\n");
	fprintf(th, "#endif\n");
	fprintf(th, "#endif\n");

	fprintf(th, "#ifndef uchar\n");
	fprintf(th, "#define uchar	unsigned char\n");
	fprintf(th, "#endif\n");
	fprintf(th, "#ifndef uint\n");
	fprintf(th, "#define uint	unsigned int\n");
	fprintf(th, "#endif\n");

	if (sizeof(void *) > 4)	/* 64 bit machine */
	{	fprintf(th, "#ifndef HASH32\n");
		fprintf(th, "#define HASH64\n");
		fprintf(th, "#endif\n");
	}
#if 0
	if (sizeof(long)==sizeof(int))
		fprintf(th, "#define long	int\n");
#endif
	if (separate == 1 && !claimproc)
	{	Symbol *n = (Symbol *) emalloc(sizeof(Symbol));
		Sequence *s = (Sequence *) emalloc(sizeof(Sequence));
		claimproc = n->name = "_:never_template:_";
		ready(n, ZN, s, 0, ZN);
	}
	if (separate == 2)
	{	if (has_remote)
		{	printf("spin: warning, make sure that the S1 model\n");
			printf("      includes the same remote references\n");
		}
		fprintf(th, "#ifndef NFAIR\n");
		fprintf(th, "#define NFAIR	2	/* must be >= 2 */\n");
		fprintf(th, "#endif\n");
		if (has_last)
		fprintf(th, "#define HAS_LAST	%d\n", has_last);
		goto doless;
	}

	fprintf(th, "#define DELTA	%d\n", DELTA);
	fprintf(th, "#ifdef MA\n");
	fprintf(th, "	#if NCORE>1 && !defined(SEP_STATE)\n");
	fprintf(th, "	#define SEP_STATE\n");
	fprintf(th, "	#endif\n");
	fprintf(th, "#if MA==1\n"); /* user typed -DMA without size */
	fprintf(th, "#undef MA\n#define MA	100\n");
	fprintf(th, "#endif\n#endif\n");
	fprintf(th, "#ifdef W_XPT\n");
	fprintf(th, "#if W_XPT==1\n"); /* user typed -DW_XPT without size */
	fprintf(th, "#undef W_XPT\n#define W_XPT 1000000\n");
	fprintf(th, "#endif\n#endif\n");
	fprintf(th, "#ifndef NFAIR\n");
	fprintf(th, "#define NFAIR	2	/* must be >= 2 */\n");
	fprintf(th, "#endif\n");
	if (Ntimeouts)
	fprintf(th, "#define NTIM	%d\n", Ntimeouts);
	if (Etimeouts)
	fprintf(th, "#define ETIM	%d\n", Etimeouts);
	if (has_remvar)
	fprintf(th, "#define REM_VARS	1\n");
	if (has_remote)
	fprintf(th, "#define REM_REFS	%d\n", has_remote); /* not yet used */
	if (has_hidden)
	fprintf(th, "#define HAS_HIDDEN	%d\n", has_hidden);
	if (has_last)
	fprintf(th, "#define HAS_LAST	%d\n", has_last);
	if (has_sorted)
	fprintf(th, "#define HAS_SORTED	%d\n", has_sorted);
	if (m_loss)
	fprintf(th, "#define M_LOSS\n");
	if (has_random)
	fprintf(th, "#define HAS_RANDOM	%d\n", has_random);
	fprintf(th, "#define HAS_CODE\n");	/* doesn't seem to cause measurable overhead */
	if (has_stack)
	fprintf(th, "#define HAS_STACK	%d\n", has_stack);
	if (has_enabled)
	fprintf(th, "#define HAS_ENABLED	1\n");
	if (has_unless)
	fprintf(th, "#define HAS_UNLESS	%d\n", has_unless);
	if (has_provided)
	fprintf(th, "#define HAS_PROVIDED	%d\n", has_provided);
	if (has_pcvalue)
	fprintf(th, "#define HAS_PCVALUE	%d\n", has_pcvalue);
	if (has_badelse)
	fprintf(th, "#define HAS_BADELSE	%d\n", has_badelse);
	if (has_enabled
	||  has_pcvalue
	||  has_badelse
	||  has_last)
	{	fprintf(th, "#ifndef NOREDUCE\n");
		fprintf(th, "#define NOREDUCE	1\n");
		fprintf(th, "#endif\n");
	}
	if (has_np)
	fprintf(th, "#define HAS_NP	%d\n", has_np);
	if (merger)
	fprintf(th, "#define MERGED	1\n");

doless:
	fprintf(th, "#ifdef NP	/* includes np_ demon */\n");
	if (!has_np)
	fprintf(th, "#define HAS_NP	2\n");
	fprintf(th, "#define VERI	%d\n",	nrRdy);
	fprintf(th, "#define endclaim	3 /* none */\n");
	fprintf(th, "#endif\n");
	if (claimproc)
	{	claimnr = fproc(claimproc);
		/* NP overrides claimproc */
		fprintf(th, "#if !defined(NOCLAIM) && !defined NP\n");
		fprintf(th, "#define VERI	%d\n",	claimnr);
		fprintf(th, "#define endclaim	endstate%d\n",	claimnr);
		fprintf(th, "#endif\n");
	}
	if (eventmap)
	{	eventmapnr = fproc(eventmap);
		fprintf(th, "#define EVENT_TRACE	%d\n",	eventmapnr);
		fprintf(th, "#define endevent	endstate%d\n",	eventmapnr);
		if (eventmap[2] == 'o')	/* ":notrace:" */
		fprintf(th, "#define NEGATED_TRACE	1\n");
	}

	fprintf(th, "typedef struct S_F_MAP {\n");
	fprintf(th, "	char *fnm; int from; int upto;\n");
	fprintf(th, "} S_F_MAP;\n");

	fprintf(tc, "/*** Generated by %s ***/\n", SpinVersion);
	fprintf(tc, "/*** From source: %s ***/\n\n", oFname->name);

	ntimes(tc, 0, 1, Pre0);

	plunk_c_decls(tc);	/* types can be refered to in State */

	switch (separate) {
	case 0:	fprintf(tc, "#include \"pan.h\"\n"); break;
	case 1:	fprintf(tc, "#include \"pan_s.h\"\n"); break;
	case 2:	fprintf(tc, "#include \"pan_t.h\"\n"); break;
	}

	fprintf(tc, "#ifdef LOOPSTATE\n");
	fprintf(tc, "double cnt_loops;\n");
	fprintf(tc, "#endif\n");

	fprintf(tc, "State	A_Root;	/* seed-state for cycles */\n");
	fprintf(tc, "State	now;	/* the full state-vector */\n");
	plunk_c_fcts(tc);	/* State can be used in fcts */

	if (separate != 2)
		ntimes(tc, 0, 1, Preamble);
	else
		fprintf(tc, "extern int verbose; extern long depth;\n");

	fprintf(tc, "#ifndef NOBOUNDCHECK\n");
	fprintf(tc, "#define Index(x, y)\tBoundcheck(x, y, II, tt, t)\n");
	fprintf(tc, "#else\n");
	fprintf(tc, "#define Index(x, y)\tx\n");
	fprintf(tc, "#endif\n");

	c_preview();	/* sets hastrack */

	for (p = rdy; p; p = p->nxt)
		mst = max(p->s->maxel, mst);

	if (separate != 2)
	{	fprintf(tt, "#ifdef PEG\n");
		fprintf(tt, "struct T_SRC {\n");
		fprintf(tt, "	char *fl; int ln;\n");
		fprintf(tt, "} T_SRC[NTRANS];\n\n");
		fprintf(tt, "void\ntr_2_src(int m, char *file, int ln)\n");
		fprintf(tt, "{	T_SRC[m].fl = file;\n");
		fprintf(tt, "	T_SRC[m].ln = ln;\n");
		fprintf(tt, "}\n\n");
		fprintf(tt, "void\nputpeg(int n, int m)\n");
		fprintf(tt, "{	printf(\"%%5d\ttrans %%4d \", m, n);\n");
		fprintf(tt, "	printf(\"file %%s line %%3d\\n\",\n");
		fprintf(tt, "		T_SRC[n].fl, T_SRC[n].ln);\n");
		fprintf(tt, "}\n");
		if (!merger)
		{	fprintf(tt, "#else\n");
			fprintf(tt, "#define tr_2_src(m,f,l)\n");
		}
		fprintf(tt, "#endif\n\n");
		fprintf(tt, "void\nsettable(void)\n{\tTrans *T;\n");
		fprintf(tt, "\tTrans *settr(int, int, int, int, int,");
		fprintf(tt, " char *, int, int, int);\n\n");
		fprintf(tt, "\ttrans = (Trans ***) ");
		fprintf(tt, "emalloc(%d*sizeof(Trans **));\n", nrRdy+1);
				/* +1 for np_ automaton */

		if (separate == 1)
		{
		fprintf(tm, "	if (II == 0)\n");
		fprintf(tm, "	{ _m = step_claim(trpt->o_pm, trpt->tau, tt, ot, t);\n");
		fprintf(tm, "	  if (_m) goto P999; else continue;\n");
		fprintf(tm, "	} else\n");
		}

		fprintf(tm, "#define rand	pan_rand\n");
		fprintf(tm, "#if defined(HAS_CODE) && defined(VERBOSE)\n");
		fprintf(tm, "	cpu_printf(\"Pr: %%d Tr: %%d\\n\", II, t->forw);\n");
		fprintf(tm, "#endif\n");
		fprintf(tm, "	switch (t->forw) {\n");
	} else
	{	fprintf(tt, "#ifndef PEG\n");
		fprintf(tt, "#define tr_2_src(m,f,l)\n");
		fprintf(tt, "#endif\n");
		fprintf(tt, "void\nset_claim(void)\n{\tTrans *T;\n");
		fprintf(tt, "\textern Trans ***trans;\n");
		fprintf(tt, "\textern Trans *settr(int, int, int, int, int,");
		fprintf(tt, " char *, int, int, int);\n\n");

		fprintf(tm, "#define rand	pan_rand\n");
		fprintf(tm, "#if defined(HAS_CODE) && defined(VERBOSE)\n");
		fprintf(tm, "	cpu_printf(\"Pr: %%d Tr: %%d\\n\", II, forw);\n");
		fprintf(tm, "#endif\n");
		fprintf(tm, "	switch (forw) {\n");
	}

	fprintf(tm, "	default: Uerror(\"bad forward move\");\n");
	fprintf(tm, "	case 0:	/* if without executable clauses */\n");
	fprintf(tm, "		continue;\n");
	fprintf(tm, "	case 1: /* generic 'goto' or 'skip' */\n");
	if (separate != 2)
		fprintf(tm, "		IfNotBlocked\n");
	fprintf(tm, "		_m = 3; goto P999;\n");
	fprintf(tm, "	case 2: /* generic 'else' */\n");
	if (separate == 2)
		fprintf(tm, "		if (o_pm&1) continue;\n");
	else
	{	fprintf(tm, "		IfNotBlocked\n");
		fprintf(tm, "		if (trpt->o_pm&1) continue;\n");
	}
	fprintf(tm, "		_m = 3; goto P999;\n");
	uniq = 3;

	if (separate == 1)
		fprintf(tb, "	if (II == 0) goto R999;\n");

	fprintf(tb, "	switch (t->back) {\n");
	fprintf(tb, "	default: Uerror(\"bad return move\");\n");
	fprintf(tb, "	case  0: goto R999; /* nothing to undo */\n");

	for (p = rdy; p; p = p->nxt)
		putproc(p);


	if (separate != 2)
	{	fprintf(th, "struct {\n");
		fprintf(th, "	int tp; short *src;\n");
		fprintf(th, "} src_all[] = {\n");
		for (p = rdy; p; p = p->nxt)
			fprintf(th, "	{ %d, &src_ln%d[0] },\n",
				p->tn, p->tn);
		fprintf(th, "	{ 0, (short *) 0 }\n");
		fprintf(th, "};\n");
		fprintf(th, "short *frm_st0;\n");	/* records src states for transitions in never claim */
	} else
	{	fprintf(th, "extern short *frm_st0;\n");
	}

	gencodetable(th);

	if (separate != 1)
	{	tm_predef_np();
		tt_predef_np();
	}
	fprintf(tt, "}\n\n");	/* end of settable() */

	fprintf(tm, "#undef rand\n");
	fprintf(tm, "	}\n\n");
	fprintf(tb, "	}\n\n");

	if (separate != 2)
	{	ntimes(tt, 0, 1, Tail);
		genheader();
		if (separate == 1)
		{	fprintf(th, "#define FORWARD_MOVES\t\"pan_s.m\"\n");
			fprintf(th, "#define REVERSE_MOVES\t\"pan_s.b\"\n");
			fprintf(th, "#define SEPARATE\n");
			fprintf(th, "#define TRANSITIONS\t\"pan_s.t\"\n");
			fprintf(th, "extern void ini_claim(int, int);\n");
		} else
		{	fprintf(th, "#define FORWARD_MOVES\t\"pan.m\"\n");
			fprintf(th, "#define REVERSE_MOVES\t\"pan.b\"\n");
			fprintf(th, "#define TRANSITIONS\t\"pan.t\"\n");
		}
		genaddproc();
		genother();
		genaddqueue();
		genunio();
		genconditionals();
		gensvmap();
		if (!run) fatal("no runable process", (char *)0);
		fprintf(tc, "void\n");
		fprintf(tc, "active_procs(void)\n{\n");
			reverse_procs(run);
		fprintf(tc, "}\n");
		ntimes(tc, 0, 1, Dfa);
		ntimes(tc, 0, 1, Xpt);

		fprintf(th, "#define NTRANS	%d\n", uniq);
		fprintf(th, "#ifdef PEG\n");
		fprintf(th, "long peg[NTRANS];\n");
		fprintf(th, "#endif\n");

		if (u_sync && !u_async)
			spit_recvs(th, tc);
	} else
	{	genheader();
		fprintf(th, "#define FORWARD_MOVES\t\"pan_t.m\"\n");
		fprintf(th, "#define REVERSE_MOVES\t\"pan_t.b\"\n");
		fprintf(th, "#define TRANSITIONS\t\"pan_t.t\"\n");
		fprintf(tc, "extern int Maxbody;\n");
		fprintf(tc, "#if VECTORSZ>32000\n");
		fprintf(tc, "extern int proc_offset[];\n");
		fprintf(tc, "#else\n");
		fprintf(tc, "extern short proc_offset[];\n");
		fprintf(tc, "#endif\n");
		fprintf(tc, "extern uchar proc_skip[];\n");