pangen6.c

这是一个同样来自贝尔实验室的和UNIX有着渊源的操作系统, 其简洁的设计和实现易于我们学习和理解

			printf(">");
			if (ca->nxt) printf(", ");
		}
		printf("\n");
	}
	printf("\n");
}

static void
AST_indirect(FSM_use *uin, FSM_trans *t, char *cause, char *pn)
{	FSM_use *u;

	/* this is a newly discovered relevant statement */
	/* all vars it uses to contribute to its DEF are new criteria */

	if (!(t->relevant&1)) AST_Changes++;

	t->round = AST_Round;
	t->relevant = 1;

	if ((verbose&32) && t->step)
	{	printf("\tDR %s [[ ", pn);
		comment(stdout, t->step->n, 0);
		printf("]]\n\t\tfully relevant %s", cause);
		if (uin) { printf(" due to "); AST_var(uin->n, uin->n->sym, 1); }
		printf("\n");
	}
	for (u = t->Val[0]; u; u = u->nxt)
		if (u != uin
		&& (u->special&(USE|DEREF_USE)))
		{	if (verbose&32)
			{	printf("\t\t\tuses(%d): ", u->special);
				AST_var(u->n, u->n->sym, 1);
				printf("\n");
			}
			name_AST_track(u->n, u->special);	/* add to slice criteria */
		}
}

static void
def_relevant(char *pn, FSM_trans *t, Lextok *n, int ischan)
{	FSM_use *u;
	ALIAS *na, *ca;
	int chanref;

	/* look for all DEF's of n
	 *	mark those stmnts relevant
	 *	mark all var USEs in those stmnts as criteria
	 */

	if (n->ntyp != ELSE)
	for (u = t->Val[0]; u; u = u->nxt)
	{	chanref = (Sym_typ(u->n) == CHAN);

		if (ischan != chanref			/* no possible match  */
		|| !(u->special&(DEF|DEREF_DEF)))	/* not a def */
			continue;

		if (AST_mutual(u->n, n, 1))
		{	AST_indirect(u, t, "(exact match)", pn);
			continue;
		}

		if (chanref)
		for (na = chalias; na; na = na->nxt)
		{	if (!AST_mutual(u->n, na->cnm, 1))
				continue;
			for (ca = na->alias; ca; ca = ca->nxt)
				if (AST_mutual(ca->cnm, n, 1)
				&&  AST_isini(ca->cnm))	
				{	AST_indirect(u, t, "(alias match)", pn);
					break;
				}
			if (ca) break;
	}	}	
}

static void
AST_relevant(Lextok *n)
{	AST *a;
	FSM_state *f;
	FSM_trans *t;
	int ischan;

	/* look for all DEF's of n
	 *	mark those stmnts relevant
	 *	mark all var USEs in those stmnts as criteria
	 */

	if (!n) return;
	ischan = (Sym_typ(n) == CHAN);

	if (verbose&32)
	{	printf("<<ast_relevant (ntyp=%d) ", n->ntyp);
		AST_var(n, n->sym, 1);
		printf(">>\n");
	}

	for (t = expl_par; t; t = t->nxt)	/* param assignments */
	{	if (!(t->relevant&1))
		def_relevant(":params:", t, n, ischan);
	}

	for (t = expl_var; t; t = t->nxt)
	{	if (!(t->relevant&1))		/* var inits */
		def_relevant(":vars:", t, n, ischan);
	}

	for (a = ast; a; a = a->nxt)		/* all other stmnts */
	{	if (strcmp(a->p->n->name, ":never:") != 0
		&&  strcmp(a->p->n->name, ":trace:") != 0
		&&  strcmp(a->p->n->name, ":notrace:") != 0)
		for (f = a->fsm; f; f = f->nxt)
		for (t = f->t; t; t = t->nxt)
		{	if (!(t->relevant&1))
			def_relevant(a->p->n->name, t, n, ischan);
	}	}
}

static int
AST_relpar(char *s)
{	FSM_trans *t, *T;
	FSM_use *u;

	for (T = expl_par; T; T = (T == expl_par)?expl_var: (FSM_trans *) 0)
	for (t = T; t; t = t->nxt)
	{	if (t->relevant&1)
		for (u = t->Val[0]; u; u = u->nxt)
		{	if (u->n->sym->type
			&&  u->n->sym->context
			&&  strcmp(u->n->sym->context->name, s) == 0)
			{
				if (verbose&32)
				{	printf("proctype %s relevant, due to symbol ", s);
					AST_var(u->n, u->n->sym, 1);
					printf("\n");
				}
				return 1;
	}	}	}
	return 0;
}

static void
AST_dorelevant(void)
{	AST *a;
	RPN *r;

	for (r = rpn; r; r = r->nxt)
	{	for (a = ast; a; a = a->nxt)
			if (strcmp(a->p->n->name, r->rn->name) == 0)
			{	a->relevant |= 1;
				break;
			}
		if (!a)
		fatal("cannot find proctype %s", r->rn->name);
	}		
}

static void
AST_procisrelevant(Symbol *s)
{	RPN *r;
	for (r = rpn; r; r = r->nxt)
		if (strcmp(r->rn->name, s->name) == 0)
			return;
	r = (RPN *) emalloc(sizeof(RPN));
	r->rn = s;
	r->nxt = rpn;
	rpn = r;
}

static int
AST_proc_isrel(char *s)
{	AST *a;

	for (a = ast; a; a = a->nxt)
		if (strcmp(a->p->n->name, s) == 0)
			return (a->relevant&1);
	non_fatal("cannot happen, missing proc in ast", (char *) 0);
	return 0;
}

static int
AST_scoutrun(Lextok *t)
{
	if (!t) return 0;

	if (t->ntyp == RUN)
		return AST_proc_isrel(t->sym->name);
	return (AST_scoutrun(t->lft) || AST_scoutrun(t->rgt));
}

static void
AST_tagruns(void)
{	AST *a;
	FSM_state *f;
	FSM_trans *t;

	/* if any stmnt inside a proctype is relevant
	 * or any parameter passed in a run
	 * then so are all the run statements on that proctype
	 */

	for (a = ast; a; a = a->nxt)
	{	if (strcmp(a->p->n->name, ":never:") == 0
		||  strcmp(a->p->n->name, ":trace:") == 0
		||  strcmp(a->p->n->name, ":notrace:") == 0
		||  strcmp(a->p->n->name, ":init:") == 0)
		{	a->relevant |= 1;	/* the proctype is relevant */
			continue;
		}
		if (AST_relpar(a->p->n->name))
			a->relevant |= 1;
		else
		{	for (f = a->fsm; f; f = f->nxt)
			for (t = f->t; t; t = t->nxt)
				if (t->relevant)
					goto yes;
yes:			if (f)
				a->relevant |= 1;
		}
	}

	for (a = ast; a; a = a->nxt)
	for (f = a->fsm; f; f = f->nxt)
	for (t = f->t; t; t = t->nxt)
		if (t->step
		&&  AST_scoutrun(t->step->n))
		{	AST_indirect((FSM_use *)0, t, ":run:", a->p->n->name);
			/* BUT, not all actual params are relevant */
		}
}

static void
AST_report(AST *a, Element *e)	/* ALSO deduce irrelevant vars */
{
	if (!(a->relevant&2))
	{	a->relevant |= 2;
		printf("spin: redundant in proctype %s (for given property):\n",
			a->p->n->name);
	}
	printf("      line %3d %s (state %d)",
		e->n?e->n->ln:-1,
		e->n?e->n->fn->name:"-",
		e->seqno);
	printf("	[");
	comment(stdout, e->n, 0);
	printf("]\n");
}

static int
AST_always(Lextok *n)
{
	if (!n) return 0;

	if (n->ntyp == '@'	/* -end */
	||  n->ntyp == 'p')	/* remote reference */
		return 1;
	return AST_always(n->lft) || AST_always(n->rgt);
}

static void
AST_edge_dump(AST *a, FSM_state *f)
{	FSM_trans *t;
	FSM_use *u;

	for (t = f->t; t; t = t->nxt)	/* edges */
	{
		if (t->step && AST_always(t->step->n))
			t->relevant |= 1;	/* always relevant */

		if (verbose&32)
		{	switch (t->relevant) {
			case  0: printf("     "); break;
			case  1: printf("*%3d ", t->round); break;
			case  2: printf("+%3d ", t->round); break;
			case  3: printf("#%3d ", t->round); break;
			default: printf("? "); break;
			}
	
			printf("%d\t->\t%d\t", f->from, t->to);
			if (t->step)
				comment(stdout, t->step->n, 0);
			else
				printf("Unless");
	
			for (u = t->Val[0]; u; u = u->nxt)
			{	printf(" <");
				AST_var(u->n, u->n->sym, 1);
				printf(":%d>", u->special);
			}
			printf("\n");
		} else
		{	if (t->relevant)
				continue;

			if (t->step)
			switch(t->step->n->ntyp) {
			case ASGN:
			case 's':
			case 'r':
			case 'c':
				if (t->step->n->lft->ntyp != CONST)
					AST_report(a, t->step);
				break;

			case PRINT:	/* don't report */
			case PRINTM:
			case ASSERT:
			case C_CODE:
			case C_EXPR:
			default:
				break;
	}	}	}
}

static void
AST_dfs(AST *a, int s, int vis)
{	FSM_state *f;
	FSM_trans *t;

	f = fsm_tbl[s];
	if (f->seen) return;

	f->seen = 1;
	if (vis) AST_edge_dump(a, f);

	for (t = f->t; t; t = t->nxt)
		AST_dfs(a, t->to, vis);
}

static void
AST_dump(AST *a)
{	FSM_state *f;

	for (f = a->fsm; f; f = f->nxt)
	{	f->seen = 0;
		fsm_tbl[f->from] = f;
	}

	if (verbose&32)
		printf("AST_START %s from %d\n", a->p->n->name, a->i_st);

	AST_dfs(a, a->i_st, 1);
}

static void
AST_sends(AST *a)
{	FSM_state *f;
	FSM_trans *t;
	FSM_use *u;
	ChanList *cl;

	for (f = a->fsm; f; f = f->nxt)		/* control states */
	for (t = f->t; t; t = t->nxt)		/* transitions    */
	{	if (t->step
		&&  t->step->n
		&&  t->step->n->ntyp == 's')
		for (u = t->Val[0]; u; u = u->nxt)
		{	if (Sym_typ(u->n) == CHAN
			&&  ((u->special&USE) && !(u->special&DEREF_USE)))
			{
#if 0
				printf("%s -- (%d->%d) -- ",
					a->p->n->name, f->from, t->to);
				AST_var(u->n, u->n->sym, 1);
				printf(" -> chanlist\n");
#endif
				cl = (ChanList *) emalloc(sizeof(ChanList));
				cl->s = t->step->n;
				cl->n = u->n;
				cl->nxt = chanlist;
				chanlist = cl;
}	}	}	}

static ALIAS *
AST_alfind(Lextok *n)
{	ALIAS *na;

	for (na = chalias; na; na = na->nxt)
		if (AST_mutual(na->cnm, n, 1))
			return na;
	return (ALIAS *) 0;
}

static void
AST_trans(void)
{	ALIAS *na, *ca, *da, *ea;
	int nchanges;

	do {
		nchanges = 0;
		for (na = chalias; na; na = na->nxt)
		{	chalcur = na;
			for (ca = na->alias; ca; ca = ca->nxt)
			{	da = AST_alfind(ca->cnm);
				if (da)
				for (ea = da->alias; ea; ea = ea->nxt)
				{	nchanges += AST_add_alias(ea->cnm,
							ea->origin|ca->origin);
		}	}	}
	} while (nchanges > 0);

	chalcur = (ALIAS *) 0;
}

static void
AST_def_use(AST *a)
{	FSM_state *f;
	FSM_trans *t;

	for (f = a->fsm; f; f = f->nxt)		/* control states */
	for (t = f->t; t; t = t->nxt)		/* all edges */
	{	cur_t = t;
		rel_use(t->Val[0]);		/* redo Val; doesn't cover structs */
		rel_use(t->Val[1]);
		t->Val[0] = t->Val[1] = (FSM_use *) 0;

		if (!t->step) continue;

		def_use(t->step->n, 0);		/* def/use info, including structs */
	}
	cur_t = (FSM_trans *) 0;
}

static void
name_AST_track(Lextok *n, int code)
{	extern int nr_errs;
#if 0
	printf("AST_name: ");
	AST_var(n, n->sym, 1);
	printf(" -- %d\n", code);
#endif
	if (in_recv && (code&DEF) && (code&USE))
	{	printf("spin: error: DEF and USE of same var in rcv stmnt: ");
		AST_var(n, n->sym, 1);
		printf(" -- %d\n", code);
		nr_errs++;
	}
	check_slice(n, code);
}

void
AST_track(Lextok *now, int code)	/* called from main.c */
{	Lextok *v; extern int export_ast;

	if (!export_ast) return;

	if (now)
	switch (now->ntyp) {
	case LEN:
	case FULL:
	case EMPTY:
	case NFULL:
	case NEMPTY:
		AST_track(now->lft, DEREF_USE|USE|code);
		break;

	case '/':
	case '*':
	case '-':
	case '+':
	case '%':
	case '&':
	case '^':
	case '|':
	case LE:
	case GE:
	case GT:
	case LT:
	case NE:
	case EQ:
	case OR:
	case AND:
	case LSHIFT:
	case RSHIFT:
		AST_track(now->rgt, USE|code);
		/* fall through */
	case '!':	
	case UMIN:	
	case '~':
	case 'c':
	case ENABLED:
	case ASSERT:
		AST_track(now->lft, USE|code);
		break;

	case EVAL:
		AST_track(now->lft, USE|(code&(~DEF)));
		break;

	case NAME:
		name_AST_track(now, code);
		if (now->sym->nel != 1)
			AST_track(now->lft, USE|code);	/* index */
		break;

	case 'R':
		AST_track(now->lft, DEREF_USE|USE|code);
		for (v = now->rgt; v; v = v->rgt)
			AST_track(v->lft, code); /* a deeper eval can add USE */
		break;

	case '?':
		AST_track(now->lft, USE|code);
		if (now->rgt)
		{	AST_track(now->rgt->lft, code);
			AST_track(now->rgt->rgt, code);
		}
		break;

/* added for control deps: */
	case TYPE:	
		name_AST_track(now, code);
		break;
	case ASGN:
		AST_track(now->lft, DEF|code);
		AST_track(now->rgt, USE|code);
		break;
	case RUN:
		name_AST_track(now, USE);
		for (v = now->lft; v; v = v->rgt)
			AST_track(v->lft, USE|code);
		break;
	case 's':
		AST_track(now->lft, DEREF_DEF|DEREF_USE|USE|code);
		for (v = now->rgt; v; v = v->rgt)
			AST_track(v->lft, USE|code);
		break;
	case 'r':
		AST_track(now->lft, DEREF_DEF|DEREF_USE|USE|code);
		for (v = now->rgt; v; v = v->rgt)
		{	in_recv++;
			AST_track(v->lft, DEF|code);
			in_recv--;
		}
		break;
	case PRINT:
		for (v = now->lft; v; v = v->rgt)
			AST_track(v->lft, USE|code);
		break;
	case PRINTM:
		AST_track(now->lft, USE);
		break;
/* end add */
	case   'p':
#if 0
			   'p' -sym-> _p
			   /
			 '?' -sym-> a (proctype)
			 /
			b (pid expr)
#endif
		AST_track(now->lft->lft, USE|code);
		AST_procisrelevant(now->lft->sym);
		break;

	case CONST:
	case ELSE:
	case NONPROGRESS:
	case PC_VAL:
	case   'q':
		break;

	case   '.':
	case  GOTO:
	case BREAK:
	case   '@':
	case D_STEP:
	case ATOMIC:
	case NON_ATOMIC:
	case IF:
	case DO:
	case UNLESS:
	case TIMEOUT:
	case C_CODE:
	case C_EXPR:
		break;

	default:
		printf("AST_track, NOT EXPECTED ntyp: %d\n", now->ntyp);
		break;
	}
}

static int
AST_dump_rel(void)
{	Slicer *rv;
	Ordered *walk;
	char buf[64];
	int banner=0;