pangen2.c

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

		fprintf(tc, "extern uchar *reached[];\n");
		fprintf(tc, "extern uchar *accpstate[];\n");
		fprintf(tc, "extern uchar *progstate[];\n");
		fprintf(tc, "extern uchar *stopstate[];\n");
		fprintf(tc, "extern uchar *visstate[];\n\n");
		fprintf(tc, "extern short *mapstate[];\n");

		fprintf(tc, "void\nini_claim(int n, int h)\n{");
		fprintf(tc, "\textern State now;\n");
		fprintf(tc, "\textern void set_claim(void);\n\n");
		fprintf(tc, "#ifdef PROV\n");
		fprintf(tc, "#include PROV\n");
		fprintf(tc, "#endif\n");
		fprintf(tc, "\tset_claim();\n");
		genother();
		fprintf(tc, "\n\tswitch (n) {\n");
		genaddproc();
		fprintf(tc, "\t}\n");
		fprintf(tc, "\n}\n");
		fprintf(tc, "int\nstep_claim(int o_pm, int tau, int tt, int ot, Trans *t)\n");
		fprintf(tc, "{	int forw = t->forw; int _m = 0; extern char *noptr; int II=0;\n");
		fprintf(tc, "	extern State now;\n");
		fprintf(tc, "#define continue	return 0\n");
		fprintf(tc, "#include \"pan_t.m\"\n");
		fprintf(tc, "P999:\n\treturn _m;\n}\n");
		fprintf(tc, "#undef continue\n");
		fprintf(tc, "int\nrev_claim(int backw)\n{ return 0; }\n");
		fprintf(tc, "#include TRANSITIONS\n");
	}
	if (separate != 1)
		ntimes(tc, 0, 1, Nvr1);

	if (separate != 2)
	{	c_wrapper(tc);
		c_chandump(tc);
	}
}

static int
find_id(Symbol *s)
{	ProcList *p;

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

static void
dolen(Symbol *s, char *pre, int pid, int ai, int qln)
{
	if (ai > 0)
		fprintf(tc, "\n\t\t\t ||    ");
	fprintf(tc, "%s(", pre);
	if (!(s->hidden&1))
	{	if (s->context)
			fprintf(tc, "((P%d *)this)->", pid);
		else
			fprintf(tc, "now.");
	}
	fprintf(tc, "%s", s->name);
	if (qln > 1) fprintf(tc, "[%d]", ai);
	fprintf(tc, ")");
}

struct AA {	char TT[9];	char CC[8]; };

static struct AA BB[4] = {
	{ "Q_FULL_F",	" q_full" },
	{ "Q_FULL_T",	"!q_full" },
	{ "Q_EMPT_F",	" !q_len" },
	{ "Q_EMPT_T",	"  q_len" }
	};

static struct AA DD[4] = {
	{ "Q_FULL_F",	" q_e_f" },	/* empty or full */
	{ "Q_FULL_T",	"!q_full" },
	{ "Q_EMPT_F",	" q_e_f" },
	{ "Q_EMPT_T",	" q_len" }
	};
	/* this reduces the number of cases where 's' and 'r'
	   are considered conditionally safe under the
	   partial order reduction rules;  as a price for
	   this simple implementation, it also affects the
	   cases where nfull and nempty can be considered
	   safe -- since these are labeled the same way as
	   's' and 'r' respectively
	   it only affects reduction, not functionality
	 */

void
bb_or_dd(int j, int which)
{
	if (which)
	{	if (has_unless)
			fprintf(tc, "%s", DD[j].CC);
		else
			fprintf(tc, "%s", BB[j].CC);
	} else
	{	if (has_unless)
			fprintf(tc, "%s", DD[j].TT);
		else
			fprintf(tc, "%s", BB[j].TT);
	}
}

void
Done_case(char *nm, Symbol *z)
{	int j, k;
	int nid = z->Nid;
	int qln = z->nel;

	fprintf(tc, "\t\tcase %d: if (", nid);
	for (j = 0; j < 4; j++)
	{	fprintf(tc, "\t(t->ty[i] == ");
		bb_or_dd(j, 0);
		fprintf(tc, " && (");
		for (k = 0; k < qln; k++)
		{	if (k > 0)
				fprintf(tc, "\n\t\t\t ||    ");
			bb_or_dd(j, 1);
			fprintf(tc, "(%s%s", nm, z->name);
			if (qln > 1)
				fprintf(tc, "[%d]", k);
			fprintf(tc, ")");
		}
		fprintf(tc, "))\n\t\t\t ");
		if (j < 3)
			fprintf(tc, "|| ");
		else
			fprintf(tc, "   ");
	}
	fprintf(tc, ") return 0; break;\n");
}

static void
Docase(Symbol *s, int pid, int nid)
{	int i, j;

	fprintf(tc, "\t\tcase %d: if (", nid);
	for (j = 0; j < 4; j++)
	{	fprintf(tc, "\t(t->ty[i] == ");
		bb_or_dd(j, 0);
		fprintf(tc, " && (");
		if (has_unless)
		{	for (i = 0; i < s->nel; i++)
				dolen(s, DD[j].CC, pid, i, s->nel);
		} else
		{	for (i = 0; i < s->nel; i++)
				dolen(s, BB[j].CC, pid, i, s->nel);
		}
		fprintf(tc, "))\n\t\t\t ");
		if (j < 3)
			fprintf(tc, "|| ");
		else
			fprintf(tc, "   ");
	}
	fprintf(tc, ") return 0; break;\n");
}

static void
genconditionals(void)
{	Symbol *s;
	int last=0, j;
	extern Ordered	*all_names;
	Ordered *walk;

	fprintf(th, "#define LOCAL	1\n");
	fprintf(th, "#define Q_FULL_F	2\n");
	fprintf(th, "#define Q_EMPT_F	3\n");
	fprintf(th, "#define Q_EMPT_T	4\n");
	fprintf(th, "#define Q_FULL_T	5\n");
	fprintf(th, "#define TIMEOUT_F	6\n");
	fprintf(th, "#define GLOBAL	7\n");
	fprintf(th, "#define BAD	8\n");
	fprintf(th, "#define ALPHA_F	9\n");

	fprintf(tc, "int\n");
	fprintf(tc, "q_cond(short II, Trans *t)\n");
	fprintf(tc, "{	int i = 0;\n");
	fprintf(tc, "	for (i = 0; i < 6; i++)\n");
	fprintf(tc, "	{	if (t->ty[i] == TIMEOUT_F) return %s;\n",
					(Etimeouts)?"(!(trpt->tau&1))":"1");
	fprintf(tc, "		if (t->ty[i] == ALPHA_F)\n");
	fprintf(tc, "#ifdef GLOB_ALPHA\n");
	fprintf(tc, "			return 0;\n");
	fprintf(tc, "#else\n\t\t\treturn ");
	fprintf(tc, "(II+1 == (short) now._nr_pr && II+1 < MAXPROC);\n");
	fprintf(tc, "#endif\n");

	/* we switch on the chan name from the spec (as identified by
	 * the corresponding Nid number) rather than the actual qid
	 * because we cannot predict at compile time which specific qid
	 * will be accessed by the statement at runtime.  that is:
	 * we do not know which qid to pass to q_cond at runtime
	 * but we do know which name is used.  if it's a chan array, we
	 * must check all elements of the array for compliance (bummer)
	 */
	fprintf(tc, "		switch (t->qu[i]) {\n");
	fprintf(tc, "		case 0: break;\n");

	for (walk = all_names; walk; walk = walk->next)
	{	s = walk->entry;
		if (s->owner) continue;
		j = find_id(s->context);
		if (s->type == CHAN)
		{	if (last == s->Nid) continue;	/* chan array */
			last = s->Nid;
			Docase(s, j, last);
		} else if (s->type == STRUCT)
		{	/* struct may contain a chan */
			char pregat[128];
			extern void walk2_struct(char *, Symbol *);
			strcpy(pregat, "");
			if (!(s->hidden&1))
			{	if (s->context)
					sprintf(pregat, "((P%d *)this)->",j);
				else
					sprintf(pregat, "now.");
			}
			walk2_struct(pregat, s);
		}
	}
	fprintf(tc, "	\tdefault: Uerror(\"unknown qid - q_cond\");\n");
	fprintf(tc, "	\t\t\treturn 0;\n");
	fprintf(tc, "	\t}\n");
	fprintf(tc, "	}\n");
	fprintf(tc, "	return 1;\n");
	fprintf(tc, "}\n");
}

static void
putproc(ProcList *p)
{	Pid = p->tn;
	Det = p->det;

	if (Pid == claimnr
	&&  separate == 1)
	{	fprintf(th, "extern uchar reached%d[];\n", Pid);
#if 0
		fprintf(th, "extern short nstates%d;\n", Pid);
#else
		fprintf(th, "\n#define nstates%d	%d\t/* %s */\n",
			Pid, p->s->maxel, p->n->name);
#endif
		fprintf(th, "extern short src_ln%d[];\n", Pid);
		fprintf(th, "extern uchar *loopstate%d;\n", Pid);
		fprintf(th, "extern S_F_MAP src_file%d[];\n", Pid);
		fprintf(th, "#define endstate%d	%d\n",
			Pid, p->s->last?p->s->last->seqno:0);
		fprintf(th, "#define src_claim	src_ln%d\n", claimnr);

		return;
	}
	if (Pid != claimnr
	&&  separate == 2)
	{	fprintf(th, "extern short src_ln%d[];\n", Pid);
		fprintf(th, "extern uchar *loopstate%d;\n", Pid);
		return;
	}

	AllGlobal = (p->prov)?1:0;	/* process has provided clause */

	fprintf(th, "\n#define nstates%d	%d\t/* %s */\n",
		Pid, p->s->maxel, p->n->name);
	if (Pid == claimnr)
	fprintf(th, "#define nstates_claim	nstates%d\n", Pid);
	if (Pid == eventmapnr)
	fprintf(th, "#define nstates_event	nstates%d\n", Pid);

	fprintf(th, "#define endstate%d	%d\n",
		Pid, p->s->last?p->s->last->seqno:0);
	fprintf(tm, "\n		 /* PROC %s */\n", p->n->name);
	fprintf(tb, "\n		 /* PROC %s */\n", p->n->name);
	fprintf(tt, "\n	/* proctype %d: %s */\n", Pid, p->n->name);
	fprintf(tt, "\n	trans[%d] = (Trans **)", Pid);
	fprintf(tt, " emalloc(%d*sizeof(Trans *));\n\n", p->s->maxel);

	if (Pid == eventmapnr)
	{	fprintf(th, "\n#define in_s_scope(x_y3_)	0");
		fprintf(tc, "\n#define in_r_scope(x_y3_)	0");
	}

	put_seq(p->s, 2, 0);
	if (Pid == eventmapnr)
	{	fprintf(th, "\n\n");
		fprintf(tc, "\n\n");
	}
	dumpsrc(p->s->maxel, Pid);
}

static void
addTpe(int x)
{	int i;

	if (x <= 2) return;

	for (i = 0; i < T_sum; i++)
		if (TPE[i] == x)
			return;
	TPE[(T_sum++)%2] = x;
}

static void
cnt_seq(Sequence *s)
{	Element *f;
	SeqList *h;

	if (s)
	for (f = s->frst; f; f = f->nxt)
	{	Tpe(f->n);	/* sets EPT */
		addTpe(EPT[0]);
		addTpe(EPT[1]);
		for (h = f->sub; h; h = h->nxt)
			cnt_seq(h->this);
		if (f == s->last)
			break;
	}
}

static void
typ_seq(Sequence *s)
{
	T_sum = 0;
	TPE[0] = 2; TPE[1] = 0;
	cnt_seq(s);
	if (T_sum > 2)		/* more than one type */
	{	TPE[0] = 5*DELTA;	/* non-mixing */
		TPE[1] = 0;
	}
}

static int
hidden(Lextok *n)
{
	if (n)
	switch (n->ntyp) {
	case  FULL: case  EMPTY:
	case NFULL: case NEMPTY: case TIMEOUT:
		Nn[(T_mus++)%2] = n;
		break;
	case '!': case UMIN: case '~': case ASSERT: case 'c':
		(void) hidden(n->lft);
		break;
	case '/': case '*': case '-': case '+':
	case '%': case LT:  case GT: case '&': case '^':
	case '|': case LE:  case GE:  case NE: case '?':
	case EQ:  case OR:  case AND: case LSHIFT: case RSHIFT:
		(void) hidden(n->lft);
		(void) hidden(n->rgt);
		break;
	}
	return T_mus;
}

static int
getNid(Lextok *n)
{
	if (n->sym
	&&  n->sym->type == STRUCT
	&&  n->rgt && n->rgt->lft)
		return getNid(n->rgt->lft);

	if (!n->sym || n->sym->Nid == 0)
	{	fatal("bad channel name '%s'",
		(n->sym)?n->sym->name:"no name");
	}
	return n->sym->Nid;
}

static int
valTpe(Lextok *n)
{	int res = 2;
	/*
	2 = local
	2+1	    .. 2+1*DELTA = nfull,  's'	- require q_full==false
	2+1+1*DELTA .. 2+2*DELTA = nempty, 'r'	- require q_len!=0
	2+1+2*DELTA .. 2+3*DELTA = empty	- require q_len==0
	2+1+3*DELTA .. 2+4*DELTA = full		- require q_full==true
	5*DELTA = non-mixing (i.e., always makes the selection global)
	6*DELTA = timeout (conditionally safe)
	7*DELTA = @, process deletion (conditionally safe)
	 */
	switch (n->ntyp) { /* a series of fall-thru cases: */
	case   FULL:	res += DELTA;		/* add 3*DELTA + chan nr */
	case  EMPTY:	res += DELTA;		/* add 2*DELTA + chan nr */
	case    'r':
	case NEMPTY:	res += DELTA;		/* add 1*DELTA + chan nr */
	case    's':
	case  NFULL:	res += getNid(n->lft);	/* add channel nr */
			break;

	case TIMEOUT:	res = 6*DELTA; break;
	case '@':	res = 7*DELTA; break;
	default:	break;
	}
	return res;
}

static void
Tpe(Lextok *n)	/* mixing in selections */
{
	EPT[0] = 2; EPT[1] = 0;

	if (!n) return;

	T_mus = 0;
	Nn[0] = Nn[1] = ZN;

	if (n->ntyp == 'c')
	{	if (hidden(n->lft) > 2)
		{	EPT[0] = 5*DELTA; /* non-mixing */
			EPT[1] = 0;
			return;
		}
	} else
		Nn[0] = n;

	if (Nn[0]) EPT[0] = valTpe(Nn[0]);
	if (Nn[1]) EPT[1] = valTpe(Nn[1]);
}

static void
put_escp(Element *e)
{	int n;
	SeqList *x;

	if (e->esc /* && e->n->ntyp != GOTO */ && e->n->ntyp != '.')
	{	for (x = e->esc, n = 0; x; x = x->nxt, n++)
		{	int i = huntele(x->this->frst, e->status, -1)->seqno;
			fprintf(tt, "\ttrans[%d][%d]->escp[%d] = %d;\n",
				Pid, e->seqno, n, i);
			fprintf(tt, "\treached%d[%d] = 1;\n",
				Pid, i);
		}
		for (x = e->esc, n=0; x; x = x->nxt, n++)
		{	fprintf(tt, "	/* escape #%d: %d */\n", n,
				huntele(x->this->frst, e->status, -1)->seqno);
			put_seq(x->this, 2, 0);	/* args?? */
		}
		fprintf(tt, "	/* end-escapes */\n");
	}
}

static void
put_sub(Element *e, int Tt0, int Tt1)
{	Sequence *s = e->n->sl->this;
	Element *g = ZE;
	int a;

	patch_atomic(s);
	putskip(s->frst->seqno);
	g = huntstart(s->frst);
	a = g->seqno;

	if (0) printf("put_sub %d -> %d -> %d\n", e->seqno, s->frst->seqno, a);

	if ((e->n->ntyp == ATOMIC
	||  e->n->ntyp == D_STEP)
	&&  scan_seq(s))
		mark_seq(s);
	s->last->nxt = e->nxt;

	typ_seq(s);	/* sets TPE */

	if (e->n->ntyp == D_STEP)
	{	int inherit = (e->status&(ATOM|L_ATOM));
		fprintf(tm, "\tcase %d: ", uniq++);
		fprintf(tm, "/* STATE %d - line %d %s - [",
			e->seqno, e->n->ln, e->n->fn->name);
		comment(tm, e->n, 0);
		fprintf(tm, "] */\n\t\t");

		if (s->last->n->ntyp == BREAK)
			OkBreak = target(huntele(s->last->nxt,
				s->last->status, -1))->Seqno;
		else
			OkBreak = -1;

		if (!putcode(tm, s, e->nxt, 0, e->n->ln, e->seqno))
		{
			fprintf(tm, "\n#if defined(C_States) && (HAS_TRACK==1)\n");
			fprintf(tm, "\t\tc_update((uchar *) &(now.c_state[0]));\n");
			fprintf(tm, "#endif\n");

			fprintf(tm, "\t\t_m = %d", getweight(s->frst->n));
			if (m_loss && s->frst->n->ntyp == 's')
				fprintf(tm, "+delta_m; delta_m = 0");
			fprintf(tm, "; goto P999;\n\n");
		}
	
		fprintf(tb, "\tcase %d: ", uniq-1);
		fprintf(tb, "/* STATE %d */\n", e->seqno);
		fprintf(tb, "\t\tsv_restor();\n");
		fprintf(tb, "\t\tgoto R999;\n");
		if (e->nxt)
			a = huntele(e->nxt, e->status, -1)->seqno;
		else
			a = 0;
		tr_map(uniq-1, e);
		fprintf(tt, "/*->*/\ttrans[%d][%d]\t= ",
			Pid, e->seqno);
		fprintf(tt, "settr(%d,%d,%d,%d,%d,\"",
			e->Seqno, D_ATOM|inherit, a, uniq-1, uniq-1);
		comment(tt, e->n, e->seqno);
		fprintf(tt, "\", %d, ", (s->frst->status&I_GLOB)?1:0);
		fprintf(tt, "%d, %d);\n", TPE[0], TPE[1]);
		put_escp(e);
	} else