flow.c

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

	for (z = s; z; prev_z = z, z = z->nxt)
		add_el(t, z->this);	/* append target */
	if (tok == DO)
	{	add_el(t, cur_s->this); /* target upfront */
		t = new_el(nn(n, BREAK, ZN, ZN)); /* break target */
		set_lab(break_dest(), t);	/* new exit  */
		breakstack = breakstack->nxt;	/* pop stack */
	}
	add_el(e, cur_s->this);
	add_el(t, cur_s->this);
	return e;			/* destination node for label */
}

static void
escape_el(Element *f, Sequence *e)
{	SeqList *z;

	for (z = f->esc; z; z = z->nxt)
		if (z->this == e)
			return;	/* already there */

	/* cover the lower-level escapes of this state */
	for (z = f->esc; z; z = z->nxt)
		attach_escape(z->this, e);

	/* now attach escape to the state itself */

	f->esc = seqlist(e, f->esc);	/* in lifo order... */
#ifdef DEBUG
	printf("attach %d (", e->frst->Seqno);
	comment(stdout, e->frst->n, 0);
	printf(")	to %d (", f->Seqno);
	comment(stdout, f->n, 0);
	printf(")\n");
#endif
	switch (f->n->ntyp) {
	case UNLESS:
		attach_escape(f->sub->this, e);
		break;
	case IF:
	case DO:
		for (z = f->sub; z; z = z->nxt)
			attach_escape(z->this, e);
		break;
	case D_STEP:
		/* attach only to the guard stmnt */
		escape_el(f->n->sl->this->frst, e);
		break;
	case ATOMIC:
	case NON_ATOMIC:
		/* attach to all stmnts */
		attach_escape(f->n->sl->this, e);
		break;
	}
}

static void
attach_escape(Sequence *n, Sequence *e)
{	Element *f;

	for (f = n->frst; f; f = f->nxt)
	{	escape_el(f, e);
		if (f == n->extent)
			break;
	}
}

static Element *
unless_seq(Lextok *n)
{	SeqList	*s  = n->sl;
	Element	*e  = new_el(ZN);
	Element	*t  = new_el(nn(ZN,'.',ZN,ZN)); /* target */
	SeqList	*z;

	e->n = nn(n, UNLESS, ZN, ZN);
	e->n->sl = s;			/* info only */
	e->sub = s;

	/* need 2 sequences: normal execution and escape */
	if (!s || !s->nxt || s->nxt->nxt)
		fatal("unexpected unless structure", (char *)0);

	/* append the target state to both */
	for (z = s; z; z = z->nxt)
		add_el(t, z->this);

	/* attach escapes to all states in normal sequence */
	attach_escape(s->this, s->nxt->this);

	add_el(e, cur_s->this);
	add_el(t, cur_s->this);
#ifdef DEBUG
	printf("unless element (%d,%d):\n", e->Seqno, t->Seqno);
	for (z = s; z; z = z->nxt)
	{	Element *x; printf("\t%d,%d,%d :: ",
		z->this->frst->Seqno,
		z->this->extent->Seqno,
		z->this->last->Seqno);
		for (x = z->this->frst; x; x = x->nxt)
			printf("(%d)", x->Seqno);
		printf("\n");
	}
#endif
	return e;
}

Element *
mk_skip(void)
{	Lextok  *t = nn(ZN, CONST, ZN, ZN);
	t->val = 1;
	return new_el(nn(ZN, 'c', t, ZN));
}

static void
add_el(Element *e, Sequence *s)
{
	if (e->n->ntyp == GOTO)
	{	Symbol *z = has_lab(e, (1|2|4));
		if (z)
		{	Element *y; /* insert a skip */
			y = mk_skip();
			mov_lab(z, e, y); /* inherit label */
			add_el(y, s);
	}	}
#ifdef DEBUG
	printf("add_el %d after %d -- ",
	e->Seqno, (s->last)?s->last->Seqno:-1);
	comment(stdout, e->n, 0);
	printf("\n");
#endif
	if (!s->frst)
		s->frst = e;
	else
		s->last->nxt = e;
	s->last = e;
}

static Element *
colons(Lextok *n)
{
	if (!n)
		return ZE;
	if (n->ntyp == ':')
	{	Element *e = colons(n->lft);
		set_lab(n->sym, e);
		return e;
	}
	innermost = n;
	return new_el(n);
}

void
add_seq(Lextok *n)
{	Element *e;

	if (!n) return;
	innermost = n;
	e = colons(n);
	if (innermost->ntyp != IF
	&&  innermost->ntyp != DO
	&&  innermost->ntyp != UNLESS)
		add_el(e, cur_s->this);
}

void
set_lab(Symbol *s, Element *e)
{	Label *l; extern Symbol *context;

	if (!s) return;
	for (l = labtab; l; l = l->nxt)
		if (l->s == s && l->c == context)
		{	non_fatal("label %s redeclared", s->name);
			break;
		}
	l = (Label *) emalloc(sizeof(Label));
	l->s = s;
	l->c = context;
	l->e = e;
	l->nxt = labtab;
	labtab = l;
}

Element *
get_lab(Lextok *n, int md)
{	Label *l;
	Symbol *s = n->sym;

	for (l = labtab; l; l = l->nxt)
		if (s == l->s)
			return (l->e);

	lineno = n->ln;
	Fname = n->fn;
	if (md) fatal("undefined label %s", s->name);
	return ZE;
}

Symbol *
has_lab(Element *e, int special)
{	Label *l;

	for (l = labtab; l; l = l->nxt)
	{	if (e != l->e)
			continue;
		if (special == 0
		||  ((special&1) && !strncmp(l->s->name, "accept", 6))
		||  ((special&2) && !strncmp(l->s->name, "end", 3))
		||  ((special&4) && !strncmp(l->s->name, "progress", 8)))
			return (l->s);
	}
	return ZS;
}

static void
mov_lab(Symbol *z, Element *e, Element *y)
{	Label *l;

	for (l = labtab; l; l = l->nxt)
		if (e == l->e)
		{	l->e = y;
			return;
		}
	if (e->n)
	{	lineno = e->n->ln;
		Fname  = e->n->fn;
	}
	fatal("cannot happen - mov_lab %s", z->name);
}

void
fix_dest(Symbol *c, Symbol *a)		/* c:label name, a:proctype name */
{	Label *l; extern Symbol *context;

#if 0
	printf("ref to label '%s' in proctype '%s', search:\n",
		c->name, a->name);
	for (l = labtab; l; l = l->nxt)
		printf("	%s in	%s\n", l->s->name, l->c->name);
#endif

	for (l = labtab; l; l = l->nxt)
	{	if (strcmp(c->name, l->s->name) == 0
		&&  strcmp(a->name, l->c->name) == 0)	/* ? */
			break;
	}
	if (!l)
	{	printf("spin: label '%s' (proctype %s)\n", c->name, a->name);
		non_fatal("unknown label '%s'", c->name);
		if (context == a)
		printf("spin: cannot remote ref a label inside the same proctype\n");
		return;
	}
	if (!l->e || !l->e->n)
		fatal("fix_dest error (%s)", c->name);
	if (l->e->n->ntyp == GOTO)
	{	Element	*y = (Element *) emalloc(sizeof(Element));
		int	keep_ln = l->e->n->ln;
		Symbol	*keep_fn = l->e->n->fn;

		/* insert skip - or target is optimized away */
		y->n = l->e->n;		  /* copy of the goto   */
		y->seqno = find_maxel(a); /* unique seqno within proc */
		y->nxt = l->e->nxt;
		y->Seqno = Unique++; y->Nxt = Al_El; Al_El = y;

		/* turn the original element+seqno into a skip */
		l->e->n = nn(ZN, 'c', nn(ZN, CONST, ZN, ZN), ZN);
		l->e->n->ln = l->e->n->lft->ln = keep_ln;
		l->e->n->fn = l->e->n->lft->fn = keep_fn;
		l->e->n->lft->val = 1;
		l->e->nxt = y;		/* append the goto  */
	}
	l->e->status |= CHECK2;	/* treat as if global */
	if (l->e->status & (ATOM | L_ATOM | D_ATOM))
	{	non_fatal("cannot reference label inside atomic or d_step (%s)",
			c->name);
	}
}

int
find_lab(Symbol *s, Symbol *c, int markit)
{	Label *l;

	for (l = labtab; l; l = l->nxt)
	{	if (strcmp(s->name, l->s->name) == 0
		&&  strcmp(c->name, l->c->name) == 0)
		{	l->visible |= markit;
			return (l->e->seqno);
	}	}
	return 0;
}

void
pushbreak(void)
{	Lbreak *r = (Lbreak *) emalloc(sizeof(Lbreak));
	Symbol *l;
	char buf[64];

	sprintf(buf, ":b%d", break_id++);
	l = lookup(buf);
	r->l = l;
	r->nxt = breakstack;
	breakstack = r;
}

Symbol *
break_dest(void)
{
	if (!breakstack)
		fatal("misplaced break statement", (char *)0);
	return breakstack->l;
}

void
make_atomic(Sequence *s, int added)
{	Element *f;

	walk_atomic(s->frst, s->last, added);

	f = s->last;
	switch (f->n->ntyp) {	/* is last step basic stmnt or sequence ? */
	case NON_ATOMIC:
	case ATOMIC:
		/* redo and search for the last step of that sequence */
		make_atomic(f->n->sl->this, added);
		break;

	case UNLESS:
		/* escapes are folded into main sequence */
		make_atomic(f->sub->this, added);
		break;

	default:
		f->status &= ~ATOM;
		f->status |= L_ATOM;
		break;
	}
}

static void
walk_atomic(Element *a, Element *b, int added)
{	Element *f; Symbol *ofn; int oln;
	SeqList *h;

	ofn = Fname;
	oln = lineno;
	for (f = a; ; f = f->nxt)
	{	f->status |= (ATOM|added);
		switch (f->n->ntyp) {
		case ATOMIC:
			if (verbose&32)
			  printf("spin: warning, line %3d %s, atomic inside %s (ignored)\n",
			  f->n->ln, f->n->fn->name, (added)?"d_step":"atomic");
			goto mknonat;
		case D_STEP:
			if (!(verbose&32))
			{	if (added) goto mknonat;
				break;
			}
			printf("spin: warning, line %3d %s, d_step inside ",
			 f->n->ln, f->n->fn->name);
			if (added)
			{	printf("d_step (ignored)\n");
				goto mknonat;
			}
			printf("atomic\n");
			break;
		case NON_ATOMIC:
mknonat:		f->n->ntyp = NON_ATOMIC; /* can jump here */
			h = f->n->sl;
			walk_atomic(h->this->frst, h->this->last, added);
			break;
		case UNLESS:
			if (added)
			{ printf("spin: error, line %3d %s, unless in d_step (ignored)\n",
			 	 f->n->ln, f->n->fn->name);
			}
		}
		for (h = f->sub; h; h = h->nxt)
			walk_atomic(h->this->frst, h->this->last, added);
		if (f == b)
			break;
	}
	Fname = ofn;
	lineno = oln;
}

void
dumplabels(void)
{	Label *l;

	for (l = labtab; l; l = l->nxt)
		if (l->c != 0 && l->s->name[0] != ':')
		printf("label	%s	%d	<%s>\n",
		l->s->name, l->e->seqno, l->c->name);
}