pangen6.c

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

	if (verbose&32)
	{	printf("Relevant variables:\n");
		for (rv = rel_vars; rv; rv = rv->nxt)
		{	printf("\t");
			AST_var(rv->n, rv->n->sym, 1);
			printf("\n");
		}
		return 1;
	}
	for (rv = rel_vars; rv; rv = rv->nxt)
		rv->n->sym->setat = 1;	/* mark it */

	for (walk = all_names; walk; walk = walk->next)
	{	Symbol *s;
		s = walk->entry;
		if (!s->setat
		&&  (s->type != MTYPE || s->ini->ntyp != CONST)
		&&  s->type != STRUCT	/* report only fields */
		&&  s->type != PROCTYPE
		&&  !s->owner
		&&  sputtype(buf, s->type))
		{	if (!banner)
			{	banner = 1;
				printf("spin: redundant vars (for given property):\n");
			}
			printf("\t");
			symvar(s);
	}	}
	return banner;
}

static void
AST_suggestions(void)
{	Symbol *s;
	Ordered *walk;
	FSM_state *f;
	FSM_trans *t;
	AST *a;
	int banner=0;
	int talked=0;

	for (walk = all_names; walk; walk = walk->next)
	{	s = walk->entry;
		if (s->colnr == 2	/* only used in conditionals */
		&&  (s->type == BYTE
		||   s->type == SHORT
		||   s->type == INT
		||   s->type == MTYPE))
		{	if (!banner)
			{	banner = 1;
				printf("spin: consider using predicate");
				printf(" abstraction to replace:\n");
			}
			printf("\t");
			symvar(s);
	}	}

	/* look for source and sink processes */

	for (a = ast; a; a = a->nxt)		/* automata       */
	{	banner = 0;
		for (f = a->fsm; f; f = f->nxt)	/* control states */
		for (t = f->t; t; t = t->nxt)	/* transitions    */
		{	if (t->step)
			switch (t->step->n->ntyp) {
			case 's':
				banner |= 1;
				break;
			case 'r':
				banner |= 2;
				break;
			case '.':
			case D_STEP:
			case ATOMIC:
			case NON_ATOMIC:
			case IF:
			case DO:
			case UNLESS:
			case '@':
			case GOTO:
			case BREAK:
			case PRINT:
			case PRINTM:
			case ASSERT:
			case C_CODE:
			case C_EXPR:
				break;
			default:
				banner |= 4;
				goto no_good;
			}
		}
no_good:	if (banner == 1 || banner == 2)
		{	printf("spin: proctype %s defines a %s process\n",
				a->p->n->name,
				banner==1?"source":"sink");
			talked |= banner;
		} else if (banner == 3)
		{	printf("spin: proctype %s mimics a buffer\n",
				a->p->n->name);
			talked |= 4;
		}
	}
	if (talked&1)
	{	printf("\tto reduce complexity, consider merging the code of\n");
		printf("\teach source process into the code of its target\n");
	}
	if (talked&2)
	{	printf("\tto reduce complexity, consider merging the code of\n");
		printf("\teach sink process into the code of its source\n");
	}
	if (talked&4)
		printf("\tto reduce complexity, avoid buffer processes\n");
}

static void
AST_preserve(void)
{	Slicer *sc, *nx, *rv;

	for (sc = slicer; sc; sc = nx)
	{	if (!sc->used)
			break;	/* done */

		nx = sc->nxt;

		for (rv = rel_vars; rv; rv = rv->nxt)
			if (AST_mutual(sc->n, rv->n, 1))
				break;

		if (!rv) /* not already there */
		{	sc->nxt = rel_vars;
			rel_vars = sc;
	}	}
	slicer = sc;
}

static void
check_slice(Lextok *n, int code)
{	Slicer *sc;

	for (sc = slicer; sc; sc = sc->nxt)
		if (AST_mutual(sc->n, n, 1)
		&&  sc->code == code)
			return;	/* already there */

	sc = (Slicer *) emalloc(sizeof(Slicer));
	sc->n = n;

	sc->code = code;
	sc->used = 0;
	sc->nxt = slicer;
	slicer = sc;
}

static void
AST_data_dep(void)
{	Slicer *sc;

	/* mark all def-relevant transitions */
	for (sc = slicer; sc; sc = sc->nxt)
	{	sc->used = 1;
		if (verbose&32)
		{	printf("spin: slice criterion ");
			AST_var(sc->n, sc->n->sym, 1);
			printf(" type=%d\n", Sym_typ(sc->n));
		}
		AST_relevant(sc->n);
	}
	AST_tagruns();	/* mark 'run's relevant if target proctype is relevant */
}

static int
AST_blockable(AST *a, int s)
{	FSM_state *f;
	FSM_trans *t;

	f = fsm_tbl[s];

	for (t = f->t; t; t = t->nxt)
	{	if (t->relevant&2)
			return 1;

		if (t->step && t->step->n)
		switch (t->step->n->ntyp) {
		case IF:
		case DO:
		case ATOMIC:
		case NON_ATOMIC:
		case D_STEP:
			if (AST_blockable(a, t->to))
			{	t->round = AST_Round;
				t->relevant |= 2;
				return 1;
			}
			/* else fall through */
		default:
			break;
		}
		else if (AST_blockable(a, t->to))	/* Unless */
		{	t->round = AST_Round;
			t->relevant |= 2;
			return 1;
		}
	}
	return 0;
}

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

	f = fsm_tbl[s];

	for (t = f->t; t; t = t->nxt)
	{	if (t->relevant&2)
			continue;

		if (t->step && t->step->n)
			switch (t->step->n->ntyp) {
			case IF:
			case DO:
			case ATOMIC:
			case NON_ATOMIC:
			case D_STEP:
				AST_spread(a, t->to);
				/* fall thru */
			default:
				t->round = AST_Round;
				t->relevant |= 2;
				break;
			}
		else	/* Unless */
		{	AST_spread(a, t->to);
			t->round = AST_Round;
			t->relevant |= 2;
		}
	}
}

static int
AST_notrelevant(Lextok *n)
{	Slicer *s;

	for (s = rel_vars; s; s = s->nxt)
		if (AST_mutual(s->n, n, 1))
			return 0;
	for (s = slicer; s; s = s->nxt)
		if (AST_mutual(s->n, n, 1))
			return 0;
	return 1;
}

static int
AST_withchan(Lextok *n)
{
	if (!n) return 0;
	if (Sym_typ(n) == CHAN)
		return 1;
	return AST_withchan(n->lft) || AST_withchan(n->rgt);
}

static int
AST_suspect(FSM_trans *t)
{	FSM_use *u;
	/* check for possible overkill */
	if (!t || !t->step || !AST_withchan(t->step->n))
		return 0;
	for (u = t->Val[0]; u; u = u->nxt)
		if (AST_notrelevant(u->n))
			return 1;
	return 0;
}

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

	f = fsm_tbl[s];
	for (t = f->t; t; t = t->nxt)
	{	if (t->step && t->step->n)
			switch (t->step->n->ntyp) {
			case IF:
			case DO:
			case ATOMIC:
			case NON_ATOMIC:
			case D_STEP:
				AST_shouldconsider(a, t->to);
				break;
			default:
				AST_track(t->step->n, 0);
/*
	AST_track is called here for a blockable stmnt from which
	a relevant stmnmt was shown to be reachable
	for a condition this makes all USEs relevant
	but for a channel operation it only makes the executability
	relevant -- in those cases, parameters that aren't already
	relevant may be replaceable with arbitrary tokens
 */
				if (AST_suspect(t))
				{	printf("spin: possibly redundant parameters in: ");
					comment(stdout, t->step->n, 0);
					printf("\n");
				}
				break;
			}
		else	/* an Unless */
			AST_shouldconsider(a, t->to);
	}
}

static int
FSM_critical(AST *a, int s)
{	FSM_state *f;
	FSM_trans *t;

	/* is a 1-relevant stmnt reachable from this state? */

	f = fsm_tbl[s];
	if (f->seen)
		goto done;
	f->seen = 1;
	f->cr   = 0;
	for (t = f->t; t; t = t->nxt)
		if ((t->relevant&1)
		||  FSM_critical(a, t->to))
		{	f->cr = 1;

			if (verbose&32)
			{	printf("\t\t\t\tcritical(%d) ", t->relevant);
				comment(stdout, t->step->n, 0);
				printf("\n");
			}
			break;
		}
#if 0
	else {
		if (verbose&32)
		{ printf("\t\t\t\tnot-crit ");
		  comment(stdout, t->step->n, 0);
	 	  printf("\n");
		}
	}
#endif
done:
	return f->cr;
}

static void
AST_ctrl(AST *a)
{	FSM_state *f;
	FSM_trans *t;
	int hit;

	/* add all blockable transitions
	 * from which relevant transitions can be reached
	 */
	if (verbose&32)
		printf("CTL -- %s\n", a->p->n->name);

	/* 1 : mark all blockable edges */
	for (f = a->fsm; f; f = f->nxt)
	{	if (!(f->scratch&2))		/* not part of irrelevant subgraph */
		for (t = f->t; t; t = t->nxt)
		{	if (t->step && t->step->n)
			switch (t->step->n->ntyp) {
			case 'r':
			case 's':
			case 'c':
			case ELSE:
				t->round = AST_Round;
				t->relevant |= 2;	/* mark for next phases */
				if (verbose&32)
				{	printf("\tpremark ");
					comment(stdout, t->step->n, 0);
					printf("\n");
				}
				break;
			default:
				break;
	}	}	}

	/* 2: keep only 2-marked stmnts from which 1-marked stmnts can be reached */
	for (f = a->fsm; f; f = f->nxt)
	{	fsm_tbl[f->from] = f;
		f->seen = 0;	/* used in dfs from FSM_critical */
	}
	for (f = a->fsm; f; f = f->nxt)
	{	if (!FSM_critical(a, f->from))
		for (t = f->t; t; t = t->nxt)
			if (t->relevant&2)
			{	t->relevant &= ~2;	/* clear mark */
				if (verbose&32)
				{	printf("\t\tnomark ");
					comment(stdout, t->step->n, 0);
					printf("\n");
	}		}	}

	/* 3 : lift marks across IF/DO etc. */
	for (f = a->fsm; f; f = f->nxt)
	{	hit = 0;
		for (t = f->t; t; t = t->nxt)
		{	if (t->step && t->step->n)
			switch (t->step->n->ntyp) {
			case IF:
			case DO:
			case ATOMIC:
			case NON_ATOMIC:
			case D_STEP:
				if (AST_blockable(a, t->to))
					hit = 1;
				break;
			default:
				break;
			}
			else if (AST_blockable(a, t->to))	/* Unless */
				hit = 1;

			if (hit) break;
		}
		if (hit)	/* at least one outgoing trans can block */
		for (t = f->t; t; t = t->nxt)
		{	t->round = AST_Round;
			t->relevant |= 2;	/* lift */
			if (verbose&32)
			{	printf("\t\t\tliftmark ");
				comment(stdout, t->step->n, 0);
				printf("\n");
			}
			AST_spread(a, t->to);	/* and spread to all guards */
	}	}

	/* 4: nodes with 2-marked out-edges contribute new slice criteria */
	for (f = a->fsm; f; f = f->nxt)
	for (t = f->t; t; t = t->nxt)
		if (t->relevant&2)
		{	AST_shouldconsider(a, f->from);
			break;	/* inner loop */
		}
}

static void
AST_control_dep(void)
{	AST *a;

	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)
			AST_ctrl(a);
}

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

	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)
		for (f = a->fsm; f; f = f->nxt)
		for (t = f->t; t; t = t->nxt)
		{	if (t->step
			&&  t->step->n
			&&  t->step->n->ntyp == ASSERT
			)
			{	t->relevant |= 1;
	}	}	}
}

static void
AST_criteria(void)
{	/*
	 * remote labels are handled separately -- by making
	 * sure they are not pruned away during optimization
	 */
	AST_Changes = 1;	/* to get started */
	for (AST_Round = 1; slicer && AST_Changes; AST_Round++)
	{	AST_Changes = 0;
		AST_data_dep();
		AST_preserve();		/* moves processed vars from slicer to rel_vars */
		AST_dominant();		/* mark data-irrelevant subgraphs */
		AST_control_dep();	/* can add data deps, which add control deps */

		if (verbose&32)
			printf("\n\nROUND %d -- changes %d\n",
				AST_Round, AST_Changes);
	}
}

static void
AST_alias_analysis(void)		/* aliasing of promela channels */
{	AST *a;

	for (a = ast; a; a = a->nxt)
		AST_sends(a);		/* collect chan-names that are send across chans */

	for (a = ast; a; a = a->nxt)
		AST_para(a->p);		/* aliasing of chans thru proctype parameters */

	for (a = ast; a; a = a->nxt)
		AST_other(a);		/* chan params in asgns and recvs */

	AST_trans();			/* transitive closure of alias table */

	if (verbose&32)
		AST_aliases();		/* show channel aliasing info */
}

void
AST_slice(void)
{	AST *a;
	int spurious = 0;

	if (!slicer)
	{	non_fatal("no slice criteria (or no claim) specified",
		(char *) 0);
		spurious = 1;
	}
	AST_dorelevant();		/* mark procs refered to in remote refs */

	for (a = ast; a; a = a->nxt)
		AST_def_use(a);		/* compute standard def/use information */

	AST_hidden();			/* parameter passing and local var inits */

	AST_alias_analysis();		/* channel alias analysis */

	AST_prelabel();			/* mark all 'assert(...)' stmnts as relevant */
	AST_criteria();			/* process the slice criteria from
					 * asserts and from the never claim
					 */
	if (!spurious || (verbose&32))
	{	spurious = 1;
		for (a = ast; a; a = a->nxt)
		{	AST_dump(a);		/* marked up result */
			if (a->relevant&2)	/* it printed something */
				spurious = 0;
		}
		if (!AST_dump_rel()		/* relevant variables */
		&&  spurious)
			printf("spin: no redundancies found (for given property)\n");
	}
	AST_suggestions();

	if (verbose&32)
		show_expl();
}

void
AST_store(ProcList *p, int start_state)
{	AST *n_ast;

	if (strcmp(p->n->name, ":never:") != 0
	&&  strcmp(p->n->name, ":trace:") != 0
	&&  strcmp(p->n->name, ":notrace:") != 0)
	{	n_ast = (AST *) emalloc(sizeof(AST));
		n_ast->p = p;
		n_ast->i_st = start_state;
		n_ast->relevant = 0;
		n_ast->fsm = fsm;
		n_ast->nxt = ast;
		ast = n_ast;
	}
	fsm = (FSM_state *) 0;	/* hide it from FSM_DEL */
}

static void
AST_add_explicit(Lextok *d, Lextok *u)
{	FSM_trans *e = (FSM_trans *) emalloc(sizeof(FSM_trans));

	e->to = 0;			/* or start_state ? */
	e->relevant = 0;		/* to be determined */
	e->step = (Element *) 0;	/* left blank */
	e->Val[0] = e->Val[1] = (FSM_use *) 0;

	cur_t = e;

	def_use(u, USE);
	def_use(d, DEF);

	cur_t = (FSM_trans *) 0;

	e->nxt = explicit;
	explicit = e;
}