pangen2.c

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

	{	/* ATOMIC or NON_ATOMIC */
		fprintf(tt, "\tT = trans[ %d][%d] = ", Pid, e->seqno);
		fprintf(tt, "settr(%d,%d,0,0,0,\"",
			e->Seqno, (e->n->ntyp == ATOMIC)?ATOM:0);
		comment(tt, e->n, e->seqno);
		if ((e->status&CHECK2)
		||  (g->status&CHECK2))
			s->frst->status |= I_GLOB;
		fprintf(tt, "\", %d, %d, %d);",
			(s->frst->status&I_GLOB)?1:0, Tt0, Tt1);
		blurb(tt, e);
		fprintf(tt, "\tT->nxt\t= ");
		fprintf(tt, "settr(%d,%d,%d,0,0,\"",
			e->Seqno, (e->n->ntyp == ATOMIC)?ATOM:0, a);
		comment(tt, e->n, e->seqno);
		fprintf(tt, "\", %d, ", (s->frst->status&I_GLOB)?1:0);
		if (e->n->ntyp == NON_ATOMIC)
		{	fprintf(tt, "%d, %d);", Tt0, Tt1);
			blurb(tt, e);
			put_seq(s, Tt0, Tt1);
		} else
		{	fprintf(tt, "%d, %d);", TPE[0], TPE[1]);
			blurb(tt, e);
			put_seq(s, TPE[0], TPE[1]);
		}
	}
}

typedef struct CaseCache {
	int m, b, owner;
	Element *e;
	Lextok *n;
	FSM_use *u;
	struct CaseCache *nxt;
} CaseCache;

static CaseCache *casing[6];

static int
identical(Lextok *p, Lextok *q)
{
	if ((!p && q) || (p && !q))
		return 0;
	if (!p)
		return 1;

	if (p->ntyp    != q->ntyp
	||  p->ismtyp  != q->ismtyp
	||  p->val     != q->val
	||  p->indstep != q->indstep
	||  p->sym     != q->sym
	||  p->sq      != q->sq
	||  p->sl      != q->sl)
		return 0;

	return	identical(p->lft, q->lft)
	&&	identical(p->rgt, q->rgt);
}

static int
samedeads(FSM_use *a, FSM_use *b)
{	FSM_use *p, *q;

	for (p = a, q = b; p && q; p = p->nxt, q = q->nxt)
		if (p->var != q->var
		||  p->special != q->special)
			return 0;
	return (!p && !q);
}

static Element *
findnext(Element *f)
{	Element *g;

	if (f->n->ntyp == GOTO)
	{	g = get_lab(f->n, 1);
		return huntele(g, f->status, -1);
	}
	return f->nxt;
}

static Element *
advance(Element *e, int stopat)
{	Element *f = e;

	if (stopat)
	while (f && f->seqno != stopat)
	{	f = findnext(f);
		if (!f)
		{	break;
		}
		switch (f->n->ntyp) {
		case GOTO:
		case '.':
		case PRINT:
		case PRINTM:
			break;
		default:
			return f;
	}	}
	return (Element *) 0;
}

static int
equiv_merges(Element *a, Element *b)
{	Element *f, *g;
	int stopat_a, stopat_b;

	if (a->merge_start)
		stopat_a = a->merge_start;
	else
		stopat_a = a->merge;

	if (b->merge_start)
		stopat_b = b->merge_start;
	else
		stopat_b = b->merge;

	if (!stopat_a && !stopat_b)
		return 1;

	for (;;)
	{
		f = advance(a, stopat_a);
		g = advance(b, stopat_b);
		if (!f && !g)
			return 1;
		if (f && g)
			return identical(f->n, g->n);
		else
			return 0;
	}
	return 1;
}

static CaseCache *
prev_case(Element *e, int owner)
{	int j; CaseCache *nc;

	switch (e->n->ntyp) {
	case 'r':	j = 0; break;
	case 's':	j = 1; break;
	case 'c':	j = 2; break;
	case ASGN:	j = 3; break;
	case ASSERT:	j = 4; break;
	default:	j = 5; break;
	}
	for (nc = casing[j]; nc; nc = nc->nxt)
		if (identical(nc->n, e->n)
		&&  samedeads(nc->u, e->dead)
		&&  equiv_merges(nc->e, e)
		&&  nc->owner == owner)
			return nc;

	return (CaseCache *) 0;
}

static void
new_case(Element *e, int m, int b, int owner)
{	int j; CaseCache *nc;

	switch (e->n->ntyp) {
	case 'r':	j = 0; break;
	case 's':	j = 1; break;
	case 'c':	j = 2; break;
	case ASGN:	j = 3; break;
	case ASSERT:	j = 4; break;
	default:	j = 5; break;
	}
	nc = (CaseCache *) emalloc(sizeof(CaseCache));
	nc->owner = owner;
	nc->m = m;
	nc->b = b;
	nc->e = e;
	nc->n = e->n;
	nc->u = e->dead;
	nc->nxt = casing[j];
	casing[j] = nc;
}

static int
nr_bup(Element *e)
{	FSM_use *u;
	Lextok *v;
	int nr = 0;

	switch (e->n->ntyp) {
	case ASGN:
		nr++;
		break;
	case  'r':
		if (e->n->val >= 1)
			nr++;	/* random recv */
		for (v = e->n->rgt; v; v = v->rgt)
		{	if ((v->lft->ntyp == CONST
			||   v->lft->ntyp == EVAL))
				continue;
			nr++;
		}
		break;
	default:
		break;
	}
	for (u = e->dead; u; u = u->nxt)
	{	switch (u->special) {
		case 2:		/* dead after write */
			if (e->n->ntyp == ASGN
			&&  e->n->rgt->ntyp == CONST
			&&  e->n->rgt->val == 0)
				break;
			nr++;
			break;
		case 1:		/* dead after read */
			nr++;
			break;
	}	}
	return nr;
}

static int
nrhops(Element *e)
{	Element *f = e, *g;
	int cnt = 0;
	int stopat;

	if (e->merge_start)
		stopat = e->merge_start;
	else
		stopat = e->merge;
#if 0
	printf("merge: %d merge_start %d - seqno %d\n",
		e->merge, e->merge_start, e->seqno);
#endif
	do {
		cnt += nr_bup(f);

		if (f->n->ntyp == GOTO)
		{	g = get_lab(f->n, 1);
			if (g->seqno == stopat)
				f = g;
			else
				f = huntele(g, f->status, stopat);
		} else
		{
			f = f->nxt;
		}

		if (f && !f->merge && !f->merge_single && f->seqno != stopat)
		{	fprintf(tm, "\n\t\tbad hop %s:%d -- at %d, <",
				f->n->fn->name,f->n->ln, f->seqno);
			comment(tm, f->n, 0);
			fprintf(tm, "> looking for %d -- merge %d:%d:%d\n\t\t",
				stopat, f->merge, f->merge_start, f->merge_single);
		 	break;
		}
	} while (f && f->seqno != stopat);

	return cnt;
}

static void
check_needed(void)
{
	if (multi_needed)
	{	fprintf(tm, "(trpt+1)->bup.ovals = grab_ints(%d);\n\t\t",
			multi_needed);
		multi_undo = multi_needed;
		multi_needed = 0;
	}
}

static void
doforward(FILE *tm_fd, Element *e)
{	FSM_use *u;

	putstmnt(tm_fd, e->n, e->seqno);

	if (e->n->ntyp != ELSE && Det)
	{	fprintf(tm_fd, ";\n\t\tif (trpt->o_pm&1)\n\t\t");
		fprintf(tm_fd, "\tuerror(\"non-determinism in D_proctype\")");
	}
	if (deadvar && !has_code)
	for (u = e->dead; u; u = u->nxt)
	{	fprintf(tm_fd, ";\n\t\t/* dead %d: %s */  ",
			u->special, u->var->name);

		switch (u->special) {
		case 2:		/* dead after write -- lval already bupped */
			if (e->n->ntyp == ASGN)	/* could be recv or asgn */
			{	if (e->n->rgt->ntyp == CONST
				&&  e->n->rgt->val == 0)
					continue;	/* already set to 0 */
			}
			if (e->n->ntyp != 'r')
			{	XZ.sym = u->var;
				fprintf(tm_fd, "\n#ifdef HAS_CODE\n");
				fprintf(tm_fd, "\t\tif (!readtrail)\n");
				fprintf(tm_fd, "#endif\n\t\t\t");
				putname(tm_fd, "", &XZ, 0, " = 0");
				break;
			} /* else fall through */
		case 1:		/* dead after read -- add asgn of rval -- needs bup */
			YZ[YZmax].sym = u->var;	/* store for pan.b */
			CnT[YZcnt]++;		/* this step added bups */
			if (multi_oval)
			{	check_needed();
				fprintf(tm_fd, "(trpt+1)->bup.ovals[%d] = ",
					multi_oval-1);
				multi_oval++;
			} else
				fprintf(tm_fd, "(trpt+1)->bup.oval = ");
			putname(tm_fd, "", &YZ[YZmax], 0, ";\n");
			fprintf(tm_fd, "#ifdef HAS_CODE\n");
			fprintf(tm_fd, "\t\tif (!readtrail)\n");
			fprintf(tm_fd, "#endif\n\t\t\t");
			putname(tm_fd, "", &YZ[YZmax], 0, " = 0");
			YZmax++;
			break;
	}	}
	fprintf(tm_fd, ";\n\t\t");
}

static int
dobackward(Element *e, int casenr)
{
	if (!any_undo(e->n) && CnT[YZcnt] == 0)
	{	YZcnt--;
		return 0;
	}

	if (!didcase)
	{	fprintf(tb, "\n\tcase %d: ", casenr);
		fprintf(tb, "/* STATE %d */\n\t\t", e->seqno);
		didcase++;
	}

	_isok++;
	while (CnT[YZcnt] > 0)	/* undo dead variable resets */
	{	CnT[YZcnt]--;
		YZmax--;
		if (YZmax < 0)
			fatal("cannot happen, dobackward", (char *)0);
		fprintf(tb, ";\n\t/* %d */\t", YZmax);
		putname(tb, "", &YZ[YZmax], 0, " = trpt->bup.oval");
		if (multi_oval > 0)
		{	multi_oval--;
			fprintf(tb, "s[%d]", multi_oval-1);
		}
	}

	if (e->n->ntyp != '.')
	{	fprintf(tb, ";\n\t\t");
		undostmnt(e->n, e->seqno);
	}
	_isok--;

	YZcnt--;
	return 1;
}

static void
lastfirst(int stopat, Element *fin, int casenr)
{	Element *f = fin, *g;

	if (f->n->ntyp == GOTO)
	{	g = get_lab(f->n, 1);
		if (g->seqno == stopat)
			f = g;
		else
			f = huntele(g, f->status, stopat);
	} else
		f = f->nxt;

	if (!f || f->seqno == stopat
	|| (!f->merge && !f->merge_single))
		return;
	lastfirst(stopat, f, casenr);
#if 0
	fprintf(tb, "\n\t/* merge %d -- %d:%d %d:%d:%d (casenr %d)	",
		YZcnt,
		f->merge_start, f->merge,
		f->seqno, f?f->seqno:-1, stopat,
		casenr);
	comment(tb, f->n, 0);
	fprintf(tb, " */\n");
	fflush(tb);
#endif
	dobackward(f, casenr);
}

static int modifier;

static void
lab_transfer(Element *to, Element *from)
{	Symbol *ns, *s = has_lab(from, (1|2|4));
	Symbol *oc;
	int ltp, usedit=0;

	if (!s) return;

	/* "from" could have all three labels -- rename
	 * to prevent jumps to the transfered copies
	 */
	oc = context;	/* remember */
	for (ltp = 1; ltp < 8; ltp *= 2)	/* 1, 2, and 4 */
		if ((s = has_lab(from, ltp)) != (Symbol *) 0)
		{	ns = (Symbol *) emalloc(sizeof(Symbol));
			ns->name = (char *) emalloc((int) strlen(s->name) + 4);
			sprintf(ns->name, "%s%d", s->name, modifier);

			context = s->context;
			set_lab(ns, to);
			usedit++;
		}
	context = oc;	/* restore */
	if (usedit)
	{	if (modifier++ > 990)
			fatal("modifier overflow error", (char *) 0);
	}
}

static int
case_cache(Element *e, int a)
{	int bupcase = 0, casenr = uniq, fromcache = 0;
	CaseCache *Cached = (CaseCache *) 0;
	Element *f, *g;
	int j, nrbups, mark, ntarget;
	extern int ccache;

	mark = (e->status&ATOM); /* could lose atomicity in a merge chain */

	if (e->merge_mark > 0
	||  (merger && e->merge_in == 0))
	{	/* state nominally unreachable (part of merge chains) */
		if (e->n->ntyp != '.'
		&&  e->n->ntyp != GOTO)
		{	fprintf(tt, "\ttrans[%d][%d]\t= ", Pid, e->seqno);
			fprintf(tt, "settr(0,0,0,0,0,\"");
			comment(tt, e->n, e->seqno);
			fprintf(tt, "\",0,0,0);\n");
		} else
		{	fprintf(tt, "\ttrans[%d][%d]\t= ", Pid, e->seqno);
			casenr = 1; /* mhs example */
			j = a;
			goto haveit; /* pakula's example */
		}

		return -1;
	}

	fprintf(tt, "\ttrans[%d][%d]\t= ", Pid, e->seqno);

	if (ccache
	&&  Pid != claimnr
	&&  Pid != eventmapnr
	&& (Cached = prev_case(e, Pid)))
	{	bupcase = Cached->b;
		casenr  = Cached->m;
		fromcache = 1;

		fprintf(tm, "/* STATE %d - line %d %s - [",
			e->seqno, e->n->ln, e->n->fn->name);
		comment(tm, e->n, 0);
		fprintf(tm, "] (%d:%d - %d) same as %d (%d:%d - %d) */\n",
			e->merge_start, e->merge, e->merge_in,
			casenr,
			Cached->e->merge_start, Cached->e->merge, Cached->e->merge_in);

		goto gotit;
	}

	fprintf(tm, "\tcase %d: /* STATE %d - line %d %s - [",
		uniq++, e->seqno, e->n->ln, e->n->fn->name);
	comment(tm, e->n, 0);
	nrbups = (e->merge || e->merge_start) ? nrhops(e) : nr_bup(e);
	fprintf(tm, "] (%d:%d:%d - %d) */\n\t\t",
		e->merge_start, e->merge, nrbups, e->merge_in);

	if (nrbups > MAXMERGE-1)
		fatal("merge requires more than 256 bups", (char *)0);

	if (e->n->ntyp != 'r' && Pid != claimnr && Pid != eventmapnr)
		fprintf(tm, "IfNotBlocked\n\t\t");

	if (multi_needed != 0 || multi_undo != 0)
		fatal("cannot happen, case_cache", (char *) 0);

	if (nrbups > 1)
	{	multi_oval = 1;
		multi_needed = nrbups; /* allocated after edge condition */
	} else
		multi_oval = 0;

	memset(CnT, 0, sizeof(CnT));
	YZmax = YZcnt = 0;

/* NEW 4.2.6 */
	if (Pid == claimnr)
	{
		fprintf(tm, "\n#if defined(VERI) && !defined(NP)\n\t\t");
		fprintf(tm, "{	static int reported%d = 0;\n\t\t", e->seqno);
		/* source state changes in retrans and must be looked up in frm_st0[t->forw] */
		fprintf(tm, "	if (verbose && !reported%d)\n\t\t", e->seqno);
		fprintf(tm, "	{	printf(\"depth %%d: Claim reached state %%d (line %%d)\\n\",\n\t\t");
		fprintf(tm, "			depth, frm_st0[t->forw], src_claim[%d]);\n\t\t", e->seqno);
		fprintf(tm, "		reported%d = 1;\n\t\t", e->seqno);
		fprintf(tm, "		fflush(stdout);\n\t\t");
		fprintf(tm, "}	}\n");
		fprintf(tm, "#endif\n\t\t");
	}