Subversion Repositories planix.SVN

Rev

Details | Last modification | View Log | RSS feed

Rev Author Line No. Line
2 - 1 
/***** spin: pangen6.c *****/
2 
 
3 
/* Copyright (c) 2000-2003 by Lucent Technologies, Bell Laboratories.     */
4 
/* All Rights Reserved.  This software is for educational purposes only.  */
5 
/* No guarantee whatsoever is expressed or implied by the distribution of */
6 
/* this code.  Permission is given to distribute this code provided that  */
7 
/* this introductory message is not removed and no monies are exchanged.  */
8 
/* Software written by Gerard J. Holzmann.  For tool documentation see:   */
9 
/*             http://spinroot.com/                                       */
10 
/* Send all bug-reports and/or questions to: bugs@spinroot.com            */
11 
 
12 
/* Abstract syntax tree analysis / slicing (spin option -A) */
13 
/* AST_store stores the fsms's for each proctype            */
14 
/* AST_track keeps track of variables used in properties    */
15 
/* AST_slice starts the slicing algorithm                   */
16 
/*      it first collects more info and then calls          */
17 
/*      AST_criteria to process the slice criteria          */
18 
 
19 
#include "spin.h"
20 
#include "y.tab.h"
21 
 
22 
extern Ordered	 *all_names;
23 
extern FSM_use   *use_free;
24 
extern FSM_state **fsm_tbl;
25 
extern FSM_state *fsm;
26 
extern int	 verbose, o_max;
27 
 
28 
static FSM_trans *cur_t;
29 
static FSM_trans *expl_par;
30 
static FSM_trans *expl_var;
31 
static FSM_trans *explicit;
32 
 
33 
extern void rel_use(FSM_use *);
34 
 
35 
#define ulong	unsigned long
36 
 
37 
typedef struct Pair {
38 
	FSM_state	*h;
39 
	int		b;
40 
	struct Pair	*nxt;
41 
} Pair;
42 
 
43 
typedef struct AST {
44 
	ProcList *p;		/* proctype decl */
45 
	int	i_st;		/* start state */
46 
	int	nstates, nwords;
47 
	int	relevant;
48 
	Pair	*pairs;		/* entry and exit nodes of proper subgraphs */
49 
	FSM_state *fsm;		/* proctype body */
50 
	struct AST *nxt;	/* linked list */
51 
} AST;
52 
 
53 
typedef struct RPN {		/* relevant proctype names */
54 
	Symbol	*rn;
55 
	struct RPN *nxt;
56 
} RPN;
57 
 
58 
typedef struct ALIAS {		/* channel aliasing info */
59 
	Lextok	*cnm;		/* this chan */
60 
	int	origin;		/* debugging - origin of the alias */
61 
	struct ALIAS	*alias;	/* can be an alias for these other chans */
62 
	struct ALIAS	*nxt;	/* linked list */
63 
} ALIAS;
64 
 
65 
typedef struct ChanList {
66 
	Lextok *s;		/* containing stmnt */
67 
	Lextok *n;		/* point of reference - could be struct */
68 
	struct ChanList *nxt;	/* linked list */
69 
} ChanList;
70 
 
71 
/* a chan alias can be created in one of three ways:
72 
	assignement to chan name
73 
		a = b -- a is now an alias for b
74 
	passing chan name as parameter in run
75 
		run x(b) -- proctype x(chan a)
76 
	passing chan name through channel
77 
		x!b -- x?a
78 
 */
79 
 
80 
#define USE		1
81 
#define DEF		2
82 
#define DEREF_DEF	4
83 
#define DEREF_USE	8
84 
 
85 
static AST	*ast;
86 
static ALIAS	*chalcur;
87 
static ALIAS	*chalias;
88 
static ChanList	*chanlist;
89 
static Slicer	*slicer;
90 
static Slicer	*rel_vars;	/* all relevant variables */
91 
static int	AST_Changes;
92 
static int	AST_Round;
93 
static RPN	*rpn;
94 
static int	in_recv = 0;
95 
 
96 
static int	AST_mutual(Lextok *, Lextok *, int);
97 
static void	AST_dominant(void);
98 
static void	AST_hidden(void);
99 
static void	AST_setcur(Lextok *);
100 
static void	check_slice(Lextok *, int);
101 
static void	curtail(AST *);
102 
static void	def_use(Lextok *, int);
103 
static void	name_AST_track(Lextok *, int);
104 
static void	show_expl(void);
105 
 
106 
static int
107 
AST_isini(Lextok *n)	/* is this an initialized channel */
108 
{	Symbol *s;
109 
 
110 
	if (!n || !n->sym) return 0;
111 
 
112 
	s = n->sym;
113 
 
114 
	if (s->type == CHAN)
115 
		return (s->ini->ntyp == CHAN); /* freshly instantiated */
116 
 
117 
	if (s->type == STRUCT && n->rgt)
118 
		return AST_isini(n->rgt->lft);
119 
 
120 
	return 0;
121 
}
122 
 
123 
static void
124 
AST_var(Lextok *n, Symbol *s, int toplevel)
125 
{
126 
	if (!s) return;
127 
 
128 
	if (toplevel)
129 
	{	if (s->context && s->type)
130 
			printf(":%s:L:", s->context->name);
131 
		else
132 
			printf("G:");
133 
	}
134 
	printf("%s", s->name); /* array indices ignored */
135 
 
136 
	if (s->type == STRUCT && n && n->rgt && n->rgt->lft)
137 
	{	printf(":");
138 
		AST_var(n->rgt->lft, n->rgt->lft->sym, 0);
139 
	}
140 
}
141 
 
142 
static void
143 
name_def_indices(Lextok *n, int code)
144 
{
145 
	if (!n || !n->sym) return;
146 
 
147 
	if (n->sym->nel > 1 || n->sym->isarray)
148 
		def_use(n->lft, code);		/* process the index */
149 
 
150 
	if (n->sym->type == STRUCT		/* and possible deeper ones */
151 
	&&  n->rgt)
152 
		name_def_indices(n->rgt->lft, code);
153 
}
154 
 
155 
static void
156 
name_def_use(Lextok *n, int code)
157 
{	FSM_use *u;
158 
 
159 
	if (!n) return;
160 
 
161 
	if ((code&USE)
162 
	&&  cur_t->step
163 
	&&  cur_t->step->n)
164 
	{	switch (cur_t->step->n->ntyp) {
165 
		case 'c': /* possible predicate abstraction? */
166 
			n->sym->colnr |= 2; /* yes */
167 
			break;
168 
		default:
169 
			n->sym->colnr |= 1; /* no  */
170 
			break;
171 
		}
172 
	}
173 
 
174 
	for (u = cur_t->Val[0]; u; u = u->nxt)
175 
		if (AST_mutual(n, u->n, 1)
176 
		&&  u->special == code)
177 
			return;
178 
 
179 
	if (use_free)
180 
	{	u = use_free;
181 
		use_free = use_free->nxt;
182 
	} else
183 
		u = (FSM_use *) emalloc(sizeof(FSM_use));
184 
 
185 
	u->n = n;
186 
	u->special = code;
187 
	u->nxt = cur_t->Val[0];
188 
	cur_t->Val[0] = u;
189 
 
190 
	name_def_indices(n, USE|(code&(~DEF)));	/* not def, but perhaps deref */
191 
}
192 
 
193 
static void
194 
def_use(Lextok *now, int code)
195 
{	Lextok *v;
196 
 
197 
	if (now)
198 
	switch (now->ntyp) {
199 
	case '!':
200 
	case UMIN:
201 
	case '~':
202 
	case 'c':
203 
	case ENABLED:
204 
	case ASSERT:
205 
	case EVAL:
206 
		def_use(now->lft, USE|code);
207 
		break;
208 
 
209 
	case LEN:
210 
	case FULL:
211 
	case EMPTY:
212 
	case NFULL:
213 
	case NEMPTY:
214 
		def_use(now->lft, DEREF_USE|USE|code);
215 
		break;
216 
 
217 
	case '/':
218 
	case '*':
219 
	case '-':
220 
	case '+':
221 
	case '%':
222 
	case '&':
223 
	case '^':
224 
	case '|':
225 
	case LE:
226 
	case GE:
227 
	case GT:
228 
	case LT:
229 
	case NE:
230 
	case EQ:
231 
	case OR:
232 
	case AND:
233 
	case LSHIFT:
234 
	case RSHIFT:
235 
		def_use(now->lft, USE|code);
236 
		def_use(now->rgt, USE|code);
237 
		break;
238 
 
239 
	case ASGN:
240 
		def_use(now->lft, DEF|code);
241 
		def_use(now->rgt, USE|code);
242 
		break;
243 
 
244 
	case TYPE:	/* name in parameter list */
245 
		name_def_use(now, code);
246 
		break;
247 
 
248 
	case NAME:
249 
		name_def_use(now, code);
250 
		break;
251 
 
252 
	case RUN:
253 
		name_def_use(now, USE);			/* procname - not really needed */
254 
		for (v = now->lft; v; v = v->rgt)
255 
			def_use(v->lft, USE);		/* params */
256 
		break;
257 
 
258 
	case 's':
259 
		def_use(now->lft, DEREF_DEF|DEREF_USE|USE|code);
260 
		for (v = now->rgt; v; v = v->rgt)
261 
			def_use(v->lft, USE|code);
262 
		break;
263 
 
264 
	case 'r':
265 
		def_use(now->lft, DEREF_DEF|DEREF_USE|USE|code);
266 
		for (v = now->rgt; v; v = v->rgt)
267 
		{	if (v->lft->ntyp == EVAL)
268 
				def_use(v->lft, code);	/* will add USE */
269 
			else if (v->lft->ntyp != CONST)
270 
				def_use(v->lft, DEF|code);
271 
		}
272 
		break;
273 
 
274 
	case 'R':
275 
		def_use(now->lft, DEREF_USE|USE|code);
276 
		for (v = now->rgt; v; v = v->rgt)
277 
		{	if (v->lft->ntyp == EVAL)
278 
				def_use(v->lft, code); /* will add USE */
279 
		}
280 
		break;
281 
 
282 
	case '?':
283 
		def_use(now->lft, USE|code);
284 
		if (now->rgt)
285 
		{	def_use(now->rgt->lft, code);
286 
			def_use(now->rgt->rgt, code);
287 
		}
288 
		break;
289 
 
290 
	case PRINT:
291 
		for (v = now->lft; v; v = v->rgt)
292 
			def_use(v->lft, USE|code);
293 
		break;
294 
 
295 
	case PRINTM:
296 
		def_use(now->lft, USE);
297 
		break;
298 
 
299 
	case CONST:
300 
	case ELSE:	/* ? */
301 
	case NONPROGRESS:
302 
	case PC_VAL:
303 
	case   'p':
304 
	case   'q':
305 
		break;
306 
 
307 
	case   '.':
308 
	case  GOTO:
309 
	case BREAK:
310 
	case   '@':
311 
	case D_STEP:
312 
	case ATOMIC:
313 
	case NON_ATOMIC:
314 
	case IF:
315 
	case DO:
316 
	case UNLESS:
317 
	case TIMEOUT:
318 
	case C_CODE:
319 
	case C_EXPR:
320 
	default:
321 
		break;
322 
	}
323 
}
324 
 
325 
static int
326 
AST_add_alias(Lextok *n, int nr)
327 
{	ALIAS *ca;
328 
	int res;
329 
 
330 
	for (ca = chalcur->alias; ca; ca = ca->nxt)
331 
		if (AST_mutual(ca->cnm, n, 1))
332 
		{	res = (ca->origin&nr);
333 
			ca->origin |= nr;	/* 1, 2, or 4 - run, asgn, or rcv */
334 
			return (res == 0);	/* 0 if already there with same origin */
335 
		}
336 
 
337 
	ca = (ALIAS *) emalloc(sizeof(ALIAS));
338 
	ca->cnm = n;
339 
	ca->origin = nr;
340 
	ca->nxt = chalcur->alias;
341 
	chalcur->alias = ca;
342 
	return 1;
343 
}
344 
 
345 
static void
346 
AST_run_alias(char *pn, char *s, Lextok *t, int parno)
347 
{	Lextok *v;
348 
	int cnt;
349 
 
350 
	if (!t) return;
351 
 
352 
	if (t->ntyp == RUN)
353 
	{	if (strcmp(t->sym->name, s) == 0)
354 
		for (v = t->lft, cnt = 1; v; v = v->rgt, cnt++)
355 
			if (cnt == parno)
356 
			{	AST_add_alias(v->lft, 1); /* RUN */
357 
				break;
358 
			}
359 
	} else
360 
	{	AST_run_alias(pn, s, t->lft, parno);
361 
		AST_run_alias(pn, s, t->rgt, parno);
362 
	}
363 
}
364 
 
365 
static void
366 
AST_findrun(char *s, int parno)
367 
{	FSM_state *f;
368 
	FSM_trans *t;
369 
	AST *a;
370 
 
371 
	for (a = ast; a; a = a->nxt)		/* automata       */
372 
	for (f = a->fsm; f; f = f->nxt)		/* control states */
373 
	for (t = f->t; t; t = t->nxt)		/* transitions    */
374 
	{	if (t->step)
375 
		AST_run_alias(a->p->n->name, s, t->step->n, parno);
376 
	}
377 
}
378 
 
379 
static void
380 
AST_par_chans(ProcList *p)	/* find local chan's init'd to chan passed as param */
381 
{	Ordered	*walk;
382 
	Symbol	*sp;
383 
 
384 
	for (walk = all_names; walk; walk = walk->next)
385 
	{	sp = walk->entry;
386 
		if (sp
387 
		&&  sp->context
388 
		&&  strcmp(sp->context->name, p->n->name) == 0
389 
		&&  sp->Nid >= 0	/* not itself a param */
390 
		&&  sp->type == CHAN
391 
		&&  sp->ini->ntyp == NAME)	/* != CONST and != CHAN */
392 
		{	Lextok *x = nn(ZN, 0, ZN, ZN);
393 
			x->sym = sp;
394 
			AST_setcur(x);
395 
			AST_add_alias(sp->ini, 2);	/* ASGN */
396 
	}	}
397 
}
398 
 
399 
static void
400 
AST_para(ProcList *p)
401 
{	Lextok *f, *t, *c;
402 
	int cnt = 0;
403 
 
404 
	AST_par_chans(p);
405 
 
406 
	for (f = p->p; f; f = f->rgt) 		/* list of types */
407 
	for (t = f->lft; t; t = t->rgt)
408 
	{	if (t->ntyp != ',')
409 
			c = t;
410 
		else
411 
			c = t->lft;	/* expanded struct */
412 
 
413 
		cnt++;
414 
		if (Sym_typ(c) == CHAN)
415 
		{	ALIAS *na = (ALIAS *) emalloc(sizeof(ALIAS));
416 
 
417 
			na->cnm = c;
418 
			na->nxt = chalias;
419 
			chalcur = chalias = na;
420 
#if 0
421 
			printf("%s -- (par) -- ", p->n->name);
422 
			AST_var(c, c->sym, 1);
423 
			printf(" => <<");
424 
#endif
425 
			AST_findrun(p->n->name, cnt);
426 
#if 0
427 
			printf(">>\n");
428 
#endif
429 
		}
430 
	}
431 
}
432 
 
433 
static void
434 
AST_haschan(Lextok *c)
435 
{
436 
	if (!c) return;
437 
	if (Sym_typ(c) == CHAN)
438 
	{	AST_add_alias(c, 2);	/* ASGN */
439 
#if 0
440 
		printf("<<");
441 
		AST_var(c, c->sym, 1);
442 
		printf(">>\n");
443 
#endif
444 
	} else
445 
	{	AST_haschan(c->rgt);
446 
		AST_haschan(c->lft);
447 
	}
448 
}
449 
 
450 
static int
451 
AST_nrpar(Lextok *n) /* 's' or 'r' */
452 
{	Lextok *m;
453 
	int j = 0;
454 
 
455 
	for (m = n->rgt; m; m = m->rgt)
456 
		j++;
457 
	return j;
458 
}
459 
 
460 
static int
461 
AST_ord(Lextok *n, Lextok *s)
462 
{	Lextok *m;
463 
	int j = 0;
464 
 
465 
	for (m = n->rgt; m; m = m->rgt)
466 
	{	j++;
467 
		if (s->sym == m->lft->sym)
468 
			return j;
469 
	}
470 
	return 0;
471 
}
472 
 
473 
#if 0
474 
static void
475 
AST_ownership(Symbol *s)
476 
{
477 
	if (!s) return;
478 
	printf("%s:", s->name);
479 
	AST_ownership(s->owner);
480 
}
481 
#endif
482 
 
483 
static int
484 
AST_mutual(Lextok *a, Lextok *b, int toplevel)
485 
{	Symbol *as, *bs;
486 
 
487 
	if (!a && !b) return 1;
488 
 
489 
	if (!a || !b) return 0;
490 
 
491 
	as = a->sym;
492 
	bs = b->sym;
493 
 
494 
	if (!as || !bs) return 0;
495 
 
496 
	if (toplevel && as->context != bs->context)
497 
		return 0;
498 
 
499 
	if (as->type != bs->type)
500 
		return 0;
501 
 
502 
	if (strcmp(as->name, bs->name) != 0)
503 
		return 0;
504 
 
505 
	if (as->type == STRUCT && a->rgt && b->rgt)	/* we know that a and b are not null */
506 
		return AST_mutual(a->rgt->lft, b->rgt->lft, 0);
507 
 
508 
	return 1;
509 
}
510 
 
511 
static void
512 
AST_setcur(Lextok *n)	/* set chalcur */
513 
{	ALIAS *ca;
514 
 
515 
	for (ca = chalias; ca; ca = ca->nxt)
516 
		if (AST_mutual(ca->cnm, n, 1))	/* if same chan */
517 
		{	chalcur = ca;
518 
			return;
519 
		}
520 
 
521 
	ca = (ALIAS *) emalloc(sizeof(ALIAS));
522 
	ca->cnm = n;
523 
	ca->nxt = chalias;
524 
	chalcur = chalias = ca;
525 
}
526 
 
527 
static void
528 
AST_other(AST *a)	/* check chan params in asgns and recvs */
529 
{	FSM_state *f;
530 
	FSM_trans *t;
531 
	FSM_use *u;
532 
	ChanList *cl;
533 
 
534 
	for (f = a->fsm; f; f = f->nxt)		/* control states */
535 
	for (t = f->t; t; t = t->nxt)		/* transitions    */
536 
	for (u = t->Val[0]; u; u = u->nxt)	/* def/use info   */
537 
		if (Sym_typ(u->n) == CHAN
538 
		&&  (u->special&DEF))		/* def of chan-name  */
539 
		{	AST_setcur(u->n);
540 
			switch (t->step->n->ntyp) {
541 
			case ASGN:
542 
				AST_haschan(t->step->n->rgt);
543 
				break;
544 
			case 'r':
545 
				/* guess sends where name may originate */
546 
				for (cl = chanlist; cl; cl = cl->nxt)	/* all sends */
547 
				{	int aa = AST_nrpar(cl->s);
548 
					int bb = AST_nrpar(t->step->n);
549 
					if (aa != bb)	/* matching nrs of params */
550 
						continue;
551 
 
552 
					aa = AST_ord(cl->s, cl->n);
553 
					bb = AST_ord(t->step->n, u->n);
554 
					if (aa != bb)	/* same position in parlist */
555 
						continue;
556 
 
557 
					AST_add_alias(cl->n, 4); /* RCV assume possible match */
558 
				}
559 
				break;
560 
			default:
561 
				printf("type = %d\n", t->step->n->ntyp);
562 
				non_fatal("unexpected chan def type", (char *) 0);
563 
				break;
564 
		}	}
565 
}
566 
 
567 
static void
568 
AST_aliases(void)
569 
{	ALIAS *na, *ca;
570 
 
571 
	for (na = chalias; na; na = na->nxt)
572 
	{	printf("\npossible aliases of ");
573 
		AST_var(na->cnm, na->cnm->sym, 1);
574 
		printf("\n\t");
575 
		for (ca = na->alias; ca; ca = ca->nxt)
576 
		{	if (!ca->cnm->sym)
577 
				printf("no valid name ");
578 
			else
579 
				AST_var(ca->cnm, ca->cnm->sym, 1);
580 
			printf("<");
581 
			if (ca->origin & 1) printf("RUN ");
582 
			if (ca->origin & 2) printf("ASGN ");
583 
			if (ca->origin & 4) printf("RCV ");
584 
			printf("[%s]", AST_isini(ca->cnm)?"Initzd":"Name");
585 
			printf(">");
586 
			if (ca->nxt) printf(", ");
587 
		}
588 
		printf("\n");
589 
	}
590 
	printf("\n");
591 
}
592 
 
593 
static void
594 
AST_indirect(FSM_use *uin, FSM_trans *t, char *cause, char *pn)
595 
{	FSM_use *u;
596 
 
597 
	/* this is a newly discovered relevant statement */
598 
	/* all vars it uses to contribute to its DEF are new criteria */
599 
 
600 
	if (!(t->relevant&1)) AST_Changes++;
601 
 
602 
	t->round = AST_Round;
603 
	t->relevant = 1;
604 
 
605 
	if ((verbose&32) && t->step)
606 
	{	printf("\tDR %s [[ ", pn);
607 
		comment(stdout, t->step->n, 0);
608 
		printf("]]\n\t\tfully relevant %s", cause);
609 
		if (uin) { printf(" due to "); AST_var(uin->n, uin->n->sym, 1); }
610 
		printf("\n");
611 
	}
612 
	for (u = t->Val[0]; u; u = u->nxt)
613 
		if (u != uin
614 
		&& (u->special&(USE|DEREF_USE)))
615 
		{	if (verbose&32)
616 
			{	printf("\t\t\tuses(%d): ", u->special);
617 
				AST_var(u->n, u->n->sym, 1);
618 
				printf("\n");
619 
			}
620 
			name_AST_track(u->n, u->special);	/* add to slice criteria */
621 
		}
622 
}
623 
 
624 
static void
625 
def_relevant(char *pn, FSM_trans *t, Lextok *n, int ischan)
626 
{	FSM_use *u;
627 
	ALIAS *na, *ca;
628 
	int chanref;
629 
 
630 
	/* look for all DEF's of n
631 
	 *	mark those stmnts relevant
632 
	 *	mark all var USEs in those stmnts as criteria
633 
	 */
634 
 
635 
	if (n->ntyp != ELSE)
636 
	for (u = t->Val[0]; u; u = u->nxt)
637 
	{	chanref = (Sym_typ(u->n) == CHAN);
638 
 
639 
		if (ischan != chanref			/* no possible match  */
640 
		|| !(u->special&(DEF|DEREF_DEF)))	/* not a def */
641 
			continue;
642 
 
643 
		if (AST_mutual(u->n, n, 1))
644 
		{	AST_indirect(u, t, "(exact match)", pn);
645 
			continue;
646 
		}
647 
 
648 
		if (chanref)
649 
		for (na = chalias; na; na = na->nxt)
650 
		{	if (!AST_mutual(u->n, na->cnm, 1))
651 
				continue;
652 
			for (ca = na->alias; ca; ca = ca->nxt)
653 
				if (AST_mutual(ca->cnm, n, 1)
654 
				&&  AST_isini(ca->cnm))
655 
				{	AST_indirect(u, t, "(alias match)", pn);
656 
					break;
657 
				}
658 
			if (ca) break;
659 
	}	}
660 
}
661 
 
662 
static void
663 
AST_relevant(Lextok *n)
664 
{	AST *a;
665 
	FSM_state *f;
666 
	FSM_trans *t;
667 
	int ischan;
668 
 
669 
	/* look for all DEF's of n
670 
	 *	mark those stmnts relevant
671 
	 *	mark all var USEs in those stmnts as criteria
672 
	 */
673 
 
674 
	if (!n) return;
675 
	ischan = (Sym_typ(n) == CHAN);
676 
 
677 
	if (verbose&32)
678 
	{	printf("<<ast_relevant (ntyp=%d) ", n->ntyp);
679 
		AST_var(n, n->sym, 1);
680 
		printf(">>\n");
681 
	}
682 
 
683 
	for (t = expl_par; t; t = t->nxt)	/* param assignments */
684 
	{	if (!(t->relevant&1))
685 
		def_relevant(":params:", t, n, ischan);
686 
	}
687 
 
688 
	for (t = expl_var; t; t = t->nxt)
689 
	{	if (!(t->relevant&1))		/* var inits */
690 
		def_relevant(":vars:", t, n, ischan);
691 
	}
692 
 
693 
	for (a = ast; a; a = a->nxt)		/* all other stmnts */
694 
	{	if (a->p->b != N_CLAIM && a->p->b != E_TRACE && a->p->b != N_TRACE)
695 
		for (f = a->fsm; f; f = f->nxt)
696 
		for (t = f->t; t; t = t->nxt)
697 
		{	if (!(t->relevant&1))
698 
			def_relevant(a->p->n->name, t, n, ischan);
699 
	}	}
700 
}
701 
 
702 
static int
703 
AST_relpar(char *s)
704 
{	FSM_trans *t, *T;
705 
	FSM_use *u;
706 
 
707 
	for (T = expl_par; T; T = (T == expl_par)?expl_var: (FSM_trans *) 0)
708 
	for (t = T; t; t = t->nxt)
709 
	{	if (t->relevant&1)
710 
		for (u = t->Val[0]; u; u = u->nxt)
711 
		{	if (u->n->sym->type
712 
			&&  u->n->sym->context
713 
			&&  strcmp(u->n->sym->context->name, s) == 0)
714 
			{
715 
				if (verbose&32)
716 
				{	printf("proctype %s relevant, due to symbol ", s);
717 
					AST_var(u->n, u->n->sym, 1);
718 
					printf("\n");
719 
				}
720 
				return 1;
721 
	}	}	}
722 
	return 0;
723 
}
724 
 
725 
static void
726 
AST_dorelevant(void)
727 
{	AST *a;
728 
	RPN *r;
729 
 
730 
	for (r = rpn; r; r = r->nxt)
731 
	{	for (a = ast; a; a = a->nxt)
732 
			if (strcmp(a->p->n->name, r->rn->name) == 0)
733 
			{	a->relevant |= 1;
734 
				break;
735 
			}
736 
		if (!a)
737 
		fatal("cannot find proctype %s", r->rn->name);
738 
	}
739 
}
740 
 
741 
static void
742 
AST_procisrelevant(Symbol *s)
743 
{	RPN *r;
744 
	for (r = rpn; r; r = r->nxt)
745 
		if (strcmp(r->rn->name, s->name) == 0)
746 
			return;
747 
	r = (RPN *) emalloc(sizeof(RPN));
748 
	r->rn = s;
749 
	r->nxt = rpn;
750 
	rpn = r;
751 
}
752 
 
753 
static int
754 
AST_proc_isrel(char *s)
755 
{	AST *a;
756 
 
757 
	for (a = ast; a; a = a->nxt)
758 
		if (strcmp(a->p->n->name, s) == 0)
759 
			return (a->relevant&1);
760 
	non_fatal("cannot happen, missing proc in ast", (char *) 0);
761 
	return 0;
762 
}
763 
 
764 
static int
765 
AST_scoutrun(Lextok *t)
766 
{
767 
	if (!t) return 0;
768 
 
769 
	if (t->ntyp == RUN)
770 
		return AST_proc_isrel(t->sym->name);
771 
	return (AST_scoutrun(t->lft) || AST_scoutrun(t->rgt));
772 
}
773 
 
774 
static void
775 
AST_tagruns(void)
776 
{	AST *a;
777 
	FSM_state *f;
778 
	FSM_trans *t;
779 
 
780 
	/* if any stmnt inside a proctype is relevant
781 
	 * or any parameter passed in a run
782 
	 * then so are all the run statements on that proctype
783 
	 */
784 
 
785 
	for (a = ast; a; a = a->nxt)
786 
	{	if (a->p->b == N_CLAIM || a->p->b == I_PROC
787 
		||  a->p->b == E_TRACE || a->p->b == N_TRACE)
788 
		{	a->relevant |= 1;	/* the proctype is relevant */
789 
			continue;
790 
		}
791 
		if (AST_relpar(a->p->n->name))
792 
			a->relevant |= 1;
793 
		else
794 
		{	for (f = a->fsm; f; f = f->nxt)
795 
			for (t = f->t; t; t = t->nxt)
796 
				if (t->relevant)
797 
					goto yes;
798 
yes:			if (f)
799 
				a->relevant |= 1;
800 
		}
801 
	}
802 
 
803 
	for (a = ast; a; a = a->nxt)
804 
	for (f = a->fsm; f; f = f->nxt)
805 
	for (t = f->t; t; t = t->nxt)
806 
		if (t->step
807 
		&&  AST_scoutrun(t->step->n))
808 
		{	AST_indirect((FSM_use *)0, t, ":run:", a->p->n->name);
809 
			/* BUT, not all actual params are relevant */
810 
		}
811 
}
812 
 
813 
static void
814 
AST_report(AST *a, Element *e)	/* ALSO deduce irrelevant vars */
815 
{
816 
	if (!(a->relevant&2))
817 
	{	a->relevant |= 2;
818 
		printf("spin: redundant in proctype %s (for given property):\n",
819 
			a->p->n->name);
820 
	}
821 
	printf("      %s:%d (state %d)",
822 
		e->n?e->n->fn->name:"-",
823 
		e->n?e->n->ln:-1,
824 
		e->seqno);
825 
	printf("	[");
826 
	comment(stdout, e->n, 0);
827 
	printf("]\n");
828 
}
829 
 
830 
static int
831 
AST_always(Lextok *n)
832 
{
833 
	if (!n) return 0;
834 
 
835 
	if (n->ntyp == '@'	/* -end */
836 
	||  n->ntyp == 'p')	/* remote reference */
837 
		return 1;
838 
	return AST_always(n->lft) || AST_always(n->rgt);
839 
}
840 
 
841 
static void
842 
AST_edge_dump(AST *a, FSM_state *f)
843 
{	FSM_trans *t;
844 
	FSM_use *u;
845 
 
846 
	for (t = f->t; t; t = t->nxt)	/* edges */
847 
	{
848 
		if (t->step && AST_always(t->step->n))
849 
			t->relevant |= 1;	/* always relevant */
850 
 
851 
		if (verbose&32)
852 
		{	switch (t->relevant) {
853 
			case  0: printf("     "); break;
854 
			case  1: printf("*%3d ", t->round); break;
855 
			case  2: printf("+%3d ", t->round); break;
856 
			case  3: printf("#%3d ", t->round); break;
857 
			default: printf("? "); break;
858 
			}
859 
 
860 
			printf("%d\t->\t%d\t", f->from, t->to);
861 
			if (t->step)
862 
				comment(stdout, t->step->n, 0);
863 
			else
864 
				printf("Unless");
865 
 
866 
			for (u = t->Val[0]; u; u = u->nxt)
867 
			{	printf(" <");
868 
				AST_var(u->n, u->n->sym, 1);
869 
				printf(":%d>", u->special);
870 
			}
871 
			printf("\n");
872 
		} else
873 
		{	if (t->relevant)
874 
				continue;
875 
 
876 
			if (t->step)
877 
			switch(t->step->n->ntyp) {
878 
			case ASGN:
879 
			case 's':
880 
			case 'r':
881 
			case 'c':
882 
				if (t->step->n->lft->ntyp != CONST)
883 
					AST_report(a, t->step);
884 
				break;
885 
 
886 
			case PRINT:	/* don't report */
887 
			case PRINTM:
888 
			case ASSERT:
889 
			case C_CODE:
890 
			case C_EXPR:
891 
			default:
892 
				break;
893 
	}	}	}
894 
}
895 
 
896 
static void
897 
AST_dfs(AST *a, int s, int vis)
898 
{	FSM_state *f;
899 
	FSM_trans *t;
900 
 
901 
	f = fsm_tbl[s];
902 
	if (f->seen) return;
903 
 
904 
	f->seen = 1;
905 
	if (vis) AST_edge_dump(a, f);
906 
 
907 
	for (t = f->t; t; t = t->nxt)
908 
		AST_dfs(a, t->to, vis);
909 
}
910 
 
911 
static void
912 
AST_dump(AST *a)
913 
{	FSM_state *f;
914 
 
915 
	for (f = a->fsm; f; f = f->nxt)
916 
	{	f->seen = 0;
917 
		fsm_tbl[f->from] = f;
918 
	}
919 
 
920 
	if (verbose&32)
921 
		printf("AST_START %s from %d\n", a->p->n->name, a->i_st);
922 
 
923 
	AST_dfs(a, a->i_st, 1);
924 
}
925 
 
926 
static void
927 
AST_sends(AST *a)
928 
{	FSM_state *f;
929 
	FSM_trans *t;
930 
	FSM_use *u;
931 
	ChanList *cl;
932 
 
933 
	for (f = a->fsm; f; f = f->nxt)		/* control states */
934 
	for (t = f->t; t; t = t->nxt)		/* transitions    */
935 
	{	if (t->step
936 
		&&  t->step->n
937 
		&&  t->step->n->ntyp == 's')
938 
		for (u = t->Val[0]; u; u = u->nxt)
939 
		{	if (Sym_typ(u->n) == CHAN
940 
			&&  ((u->special&USE) && !(u->special&DEREF_USE)))
941 
			{
942 
#if 0
943 
				printf("%s -- (%d->%d) -- ",
944 
					a->p->n->name, f->from, t->to);
945 
				AST_var(u->n, u->n->sym, 1);
946 
				printf(" -> chanlist\n");
947 
#endif
948 
				cl = (ChanList *) emalloc(sizeof(ChanList));
949 
				cl->s = t->step->n;
950 
				cl->n = u->n;
951 
				cl->nxt = chanlist;
952 
				chanlist = cl;
953 
}	}	}	}
954 
 
955 
static ALIAS *
956 
AST_alfind(Lextok *n)
957 
{	ALIAS *na;
958 
 
959 
	for (na = chalias; na; na = na->nxt)
960 
		if (AST_mutual(na->cnm, n, 1))
961 
			return na;
962 
	return (ALIAS *) 0;
963 
}
964 
 
965 
static void
966 
AST_trans(void)
967 
{	ALIAS *na, *ca, *da, *ea;
968 
	int nchanges;
969 
 
970 
	do {
971 
		nchanges = 0;
972 
		for (na = chalias; na; na = na->nxt)
973 
		{	chalcur = na;
974 
			for (ca = na->alias; ca; ca = ca->nxt)
975 
			{	da = AST_alfind(ca->cnm);
976 
				if (da)
977 
				for (ea = da->alias; ea; ea = ea->nxt)
978 
				{	nchanges += AST_add_alias(ea->cnm,
979 
							ea->origin|ca->origin);
980 
		}	}	}
981 
	} while (nchanges > 0);
982 
 
983 
	chalcur = (ALIAS *) 0;
984 
}
985 
 
986 
static void
987 
AST_def_use(AST *a)
988 
{	FSM_state *f;
989 
	FSM_trans *t;
990 
 
991 
	for (f = a->fsm; f; f = f->nxt)		/* control states */
992 
	for (t = f->t; t; t = t->nxt)		/* all edges */
993 
	{	cur_t = t;
994 
		rel_use(t->Val[0]);		/* redo Val; doesn't cover structs */
995 
		rel_use(t->Val[1]);
996 
		t->Val[0] = t->Val[1] = (FSM_use *) 0;
997 
 
998 
		if (!t->step) continue;
999 
 
1000 
		def_use(t->step->n, 0);		/* def/use info, including structs */
1001 
	}
1002 
	cur_t = (FSM_trans *) 0;
1003 
}
1004 
 
1005 
static void
1006 
name_AST_track(Lextok *n, int code)
1007 
{	extern int nr_errs;
1008 
#if 0
1009 
	printf("AST_name: ");
1010 
	AST_var(n, n->sym, 1);
1011 
	printf(" -- %d\n", code);
1012 
#endif
1013 
	if (in_recv && (code&DEF) && (code&USE))
1014 
	{	printf("spin: error: DEF and USE of same var in rcv stmnt: ");
1015 
		AST_var(n, n->sym, 1);
1016 
		printf(" -- %d\n", code);
1017 
		nr_errs++;
1018 
	}
1019 
	check_slice(n, code);
1020 
}
1021 
 
1022 
void
1023 
AST_track(Lextok *now, int code)	/* called from main.c */
1024 
{	Lextok *v; extern int export_ast;
1025 
 
1026 
	if (!export_ast) return;
1027 
 
1028 
	if (now)
1029 
	switch (now->ntyp) {
1030 
	case LEN:
1031 
	case FULL:
1032 
	case EMPTY:
1033 
	case NFULL:
1034 
	case NEMPTY:
1035 
		AST_track(now->lft, DEREF_USE|USE|code);
1036 
		break;
1037 
 
1038 
	case '/':
1039 
	case '*':
1040 
	case '-':
1041 
	case '+':
1042 
	case '%':
1043 
	case '&':
1044 
	case '^':
1045 
	case '|':
1046 
	case LE:
1047 
	case GE:
1048 
	case GT:
1049 
	case LT:
1050 
	case NE:
1051 
	case EQ:
1052 
	case OR:
1053 
	case AND:
1054 
	case LSHIFT:
1055 
	case RSHIFT:
1056 
		AST_track(now->rgt, USE|code);
1057 
		/* fall through */
1058 
	case '!':
1059 
	case UMIN:
1060 
	case '~':
1061 
	case 'c':
1062 
	case ENABLED:
1063 
	case ASSERT:
1064 
		AST_track(now->lft, USE|code);
1065 
		break;
1066 
 
1067 
	case EVAL:
1068 
		AST_track(now->lft, USE|(code&(~DEF)));
1069 
		break;
1070 
 
1071 
	case NAME:
1072 
		name_AST_track(now, code);
1073 
		if (now->sym->nel > 1 || now->sym->isarray)
1074 
			AST_track(now->lft, USE|code);	/* index */
1075 
		break;
1076 
 
1077 
	case 'R':
1078 
		AST_track(now->lft, DEREF_USE|USE|code);
1079 
		for (v = now->rgt; v; v = v->rgt)
1080 
			AST_track(v->lft, code); /* a deeper eval can add USE */
1081 
		break;
1082 
 
1083 
	case '?':
1084 
		AST_track(now->lft, USE|code);
1085 
		if (now->rgt)
1086 
		{	AST_track(now->rgt->lft, code);
1087 
			AST_track(now->rgt->rgt, code);
1088 
		}
1089 
		break;
1090 
 
1091 
/* added for control deps: */
1092 
	case TYPE:
1093 
		name_AST_track(now, code);
1094 
		break;
1095 
	case ASGN:
1096 
		AST_track(now->lft, DEF|code);
1097 
		AST_track(now->rgt, USE|code);
1098 
		break;
1099 
	case RUN:
1100 
		name_AST_track(now, USE);
1101 
		for (v = now->lft; v; v = v->rgt)
1102 
			AST_track(v->lft, USE|code);
1103 
		break;
1104 
	case 's':
1105 
		AST_track(now->lft, DEREF_DEF|DEREF_USE|USE|code);
1106 
		for (v = now->rgt; v; v = v->rgt)
1107 
			AST_track(v->lft, USE|code);
1108 
		break;
1109 
	case 'r':
1110 
		AST_track(now->lft, DEREF_DEF|DEREF_USE|USE|code);
1111 
		for (v = now->rgt; v; v = v->rgt)
1112 
		{	in_recv++;
1113 
			AST_track(v->lft, DEF|code);
1114 
			in_recv--;
1115 
		}
1116 
		break;
1117 
	case PRINT:
1118 
		for (v = now->lft; v; v = v->rgt)
1119 
			AST_track(v->lft, USE|code);
1120 
		break;
1121 
	case PRINTM:
1122 
		AST_track(now->lft, USE);
1123 
		break;
1124 
/* end add */
1125 
	case   'p':
1126 
#if 0
1127 
			   'p' -sym-> _p
1128 
			   /
1129 
			 '?' -sym-> a (proctype)
1130 
			 /
1131 
			b (pid expr)
1132 
#endif
1133 
		AST_track(now->lft->lft, USE|code);
1134 
		AST_procisrelevant(now->lft->sym);
1135 
		break;
1136 
 
1137 
	case CONST:
1138 
	case ELSE:
1139 
	case NONPROGRESS:
1140 
	case PC_VAL:
1141 
	case   'q':
1142 
		break;
1143 
 
1144 
	case   '.':
1145 
	case  GOTO:
1146 
	case BREAK:
1147 
	case   '@':
1148 
	case D_STEP:
1149 
	case ATOMIC:
1150 
	case NON_ATOMIC:
1151 
	case IF:
1152 
	case DO:
1153 
	case UNLESS:
1154 
	case TIMEOUT:
1155 
	case C_CODE:
1156 
	case C_EXPR:
1157 
		break;
1158 
 
1159 
	default:
1160 
		printf("AST_track, NOT EXPECTED ntyp: %d\n", now->ntyp);
1161 
		break;
1162 
	}
1163 
}
1164 
 
1165 
static int
1166 
AST_dump_rel(void)
1167 
{	Slicer *rv;
1168 
	Ordered *walk;
1169 
	char buf[64];
1170 
	int banner=0;
1171 
 
1172 
	if (verbose&32)
1173 
	{	printf("Relevant variables:\n");
1174 
		for (rv = rel_vars; rv; rv = rv->nxt)
1175 
		{	printf("\t");
1176 
			AST_var(rv->n, rv->n->sym, 1);
1177 
			printf("\n");
1178 
		}
1179 
		return 1;
1180 
	}
1181 
	for (rv = rel_vars; rv; rv = rv->nxt)
1182 
		rv->n->sym->setat = 1;	/* mark it */
1183 
 
1184 
	for (walk = all_names; walk; walk = walk->next)
1185 
	{	Symbol *s;
1186 
		s = walk->entry;
1187 
		if (!s->setat
1188 
		&&  (s->type != MTYPE || s->ini->ntyp != CONST)
1189 
		&&  s->type != STRUCT	/* report only fields */
1190 
		&&  s->type != PROCTYPE
1191 
		&&  !s->owner
1192 
		&&  sputtype(buf, s->type))
1193 
		{	if (!banner)
1194 
			{	banner = 1;
1195 
				printf("spin: redundant vars (for given property):\n");
1196 
			}
1197 
			printf("\t");
1198 
			symvar(s);
1199 
	}	}
1200 
	return banner;
1201 
}
1202 
 
1203 
static void
1204 
AST_suggestions(void)
1205 
{	Symbol *s;
1206 
	Ordered *walk;
1207 
	FSM_state *f;
1208 
	FSM_trans *t;
1209 
	AST *a;
1210 
	int banner=0;
1211 
	int talked=0;
1212 
 
1213 
	for (walk = all_names; walk; walk = walk->next)
1214 
	{	s = walk->entry;
1215 
		if (s->colnr == 2	/* only used in conditionals */
1216 
		&&  (s->type == BYTE
1217 
		||   s->type == SHORT
1218 
		||   s->type == INT
1219 
		||   s->type == MTYPE))
1220 
		{	if (!banner)
1221 
			{	banner = 1;
1222 
				printf("spin: consider using predicate");
1223 
				printf(" abstraction to replace:\n");
1224 
			}
1225 
			printf("\t");
1226 
			symvar(s);
1227 
	}	}
1228 
 
1229 
	/* look for source and sink processes */
1230 
 
1231 
	for (a = ast; a; a = a->nxt)		/* automata       */
1232 
	{	banner = 0;
1233 
		for (f = a->fsm; f; f = f->nxt)	/* control states */
1234 
		for (t = f->t; t; t = t->nxt)	/* transitions    */
1235 
		{	if (t->step)
1236 
			switch (t->step->n->ntyp) {
1237 
			case 's':
1238 
				banner |= 1;
1239 
				break;
1240 
			case 'r':
1241 
				banner |= 2;
1242 
				break;
1243 
			case '.':
1244 
			case D_STEP:
1245 
			case ATOMIC:
1246 
			case NON_ATOMIC:
1247 
			case IF:
1248 
			case DO:
1249 
			case UNLESS:
1250 
			case '@':
1251 
			case GOTO:
1252 
			case BREAK:
1253 
			case PRINT:
1254 
			case PRINTM:
1255 
			case ASSERT:
1256 
			case C_CODE:
1257 
			case C_EXPR:
1258 
				break;
1259 
			default:
1260 
				banner |= 4;
1261 
				goto no_good;
1262 
			}
1263 
		}
1264 
no_good:	if (banner == 1 || banner == 2)
1265 
		{	printf("spin: proctype %s defines a %s process\n",
1266 
				a->p->n->name,
1267 
				banner==1?"source":"sink");
1268 
			talked |= banner;
1269 
		} else if (banner == 3)
1270 
		{	printf("spin: proctype %s mimics a buffer\n",
1271 
				a->p->n->name);
1272 
			talked |= 4;
1273 
		}
1274 
	}
1275 
	if (talked&1)
1276 
	{	printf("\tto reduce complexity, consider merging the code of\n");
1277 
		printf("\teach source process into the code of its target\n");
1278 
	}
1279 
	if (talked&2)
1280 
	{	printf("\tto reduce complexity, consider merging the code of\n");
1281 
		printf("\teach sink process into the code of its source\n");
1282 
	}
1283 
	if (talked&4)
1284 
		printf("\tto reduce complexity, avoid buffer processes\n");
1285 
}
1286 
 
1287 
static void
1288 
AST_preserve(void)
1289 
{	Slicer *sc, *nx, *rv;
1290 
 
1291 
	for (sc = slicer; sc; sc = nx)
1292 
	{	if (!sc->used)
1293 
			break;	/* done */
1294 
 
1295 
		nx = sc->nxt;
1296 
 
1297 
		for (rv = rel_vars; rv; rv = rv->nxt)
1298 
			if (AST_mutual(sc->n, rv->n, 1))
1299 
				break;
1300 
 
1301 
		if (!rv) /* not already there */
1302 
		{	sc->nxt = rel_vars;
1303 
			rel_vars = sc;
1304 
	}	}
1305 
	slicer = sc;
1306 
}
1307 
 
1308 
static void
1309 
check_slice(Lextok *n, int code)
1310 
{	Slicer *sc;
1311 
 
1312 
	for (sc = slicer; sc; sc = sc->nxt)
1313 
		if (AST_mutual(sc->n, n, 1)
1314 
		&&  sc->code == code)
1315 
			return;	/* already there */
1316 
 
1317 
	sc = (Slicer *) emalloc(sizeof(Slicer));
1318 
	sc->n = n;
1319 
 
1320 
	sc->code = code;
1321 
	sc->used = 0;
1322 
	sc->nxt = slicer;
1323 
	slicer = sc;
1324 
}
1325 
 
1326 
static void
1327 
AST_data_dep(void)
1328 
{	Slicer *sc;
1329 
 
1330 
	/* mark all def-relevant transitions */
1331 
	for (sc = slicer; sc; sc = sc->nxt)
1332 
	{	sc->used = 1;
1333 
		if (verbose&32)
1334 
		{	printf("spin: slice criterion ");
1335 
			AST_var(sc->n, sc->n->sym, 1);
1336 
			printf(" type=%d\n", Sym_typ(sc->n));
1337 
		}
1338 
		AST_relevant(sc->n);
1339 
	}
1340 
	AST_tagruns();	/* mark 'run's relevant if target proctype is relevant */
1341 
}
1342 
 
1343 
static int
1344 
AST_blockable(AST *a, int s)
1345 
{	FSM_state *f;
1346 
	FSM_trans *t;
1347 
 
1348 
	f = fsm_tbl[s];
1349 
 
1350 
	for (t = f->t; t; t = t->nxt)
1351 
	{	if (t->relevant&2)
1352 
			return 1;
1353 
 
1354 
		if (t->step && t->step->n)
1355 
		switch (t->step->n->ntyp) {
1356 
		case IF:
1357 
		case DO:
1358 
		case ATOMIC:
1359 
		case NON_ATOMIC:
1360 
		case D_STEP:
1361 
			if (AST_blockable(a, t->to))
1362 
			{	t->round = AST_Round;
1363 
				t->relevant |= 2;
1364 
				return 1;
1365 
			}
1366 
			/* else fall through */
1367 
		default:
1368 
			break;
1369 
		}
1370 
		else if (AST_blockable(a, t->to))	/* Unless */
1371 
		{	t->round = AST_Round;
1372 
			t->relevant |= 2;
1373 
			return 1;
1374 
		}
1375 
	}
1376 
	return 0;
1377 
}
1378 
 
1379 
static void
1380 
AST_spread(AST *a, int s)
1381 
{	FSM_state *f;
1382 
	FSM_trans *t;
1383 
 
1384 
	f = fsm_tbl[s];
1385 
 
1386 
	for (t = f->t; t; t = t->nxt)
1387 
	{	if (t->relevant&2)
1388 
			continue;
1389 
 
1390 
		if (t->step && t->step->n)
1391 
			switch (t->step->n->ntyp) {
1392 
			case IF:
1393 
			case DO:
1394 
			case ATOMIC:
1395 
			case NON_ATOMIC:
1396 
			case D_STEP:
1397 
				AST_spread(a, t->to);
1398 
				/* fall thru */
1399 
			default:
1400 
				t->round = AST_Round;
1401 
				t->relevant |= 2;
1402 
				break;
1403 
			}
1404 
		else	/* Unless */
1405 
		{	AST_spread(a, t->to);
1406 
			t->round = AST_Round;
1407 
			t->relevant |= 2;
1408 
		}
1409 
	}
1410 
}
1411 
 
1412 
static int
1413 
AST_notrelevant(Lextok *n)
1414 
{	Slicer *s;
1415 
 
1416 
	for (s = rel_vars; s; s = s->nxt)
1417 
		if (AST_mutual(s->n, n, 1))
1418 
			return 0;
1419 
	for (s = slicer; s; s = s->nxt)
1420 
		if (AST_mutual(s->n, n, 1))
1421 
			return 0;
1422 
	return 1;
1423 
}
1424 
 
1425 
static int
1426 
AST_withchan(Lextok *n)
1427 
{
1428 
	if (!n) return 0;
1429 
	if (Sym_typ(n) == CHAN)
1430 
		return 1;
1431 
	return AST_withchan(n->lft) || AST_withchan(n->rgt);
1432 
}
1433 
 
1434 
static int
1435 
AST_suspect(FSM_trans *t)
1436 
{	FSM_use *u;
1437 
	/* check for possible overkill */
1438 
	if (!t || !t->step || !AST_withchan(t->step->n))
1439 
		return 0;
1440 
	for (u = t->Val[0]; u; u = u->nxt)
1441 
		if (AST_notrelevant(u->n))
1442 
			return 1;
1443 
	return 0;
1444 
}
1445 
 
1446 
static void
1447 
AST_shouldconsider(AST *a, int s)
1448 
{	FSM_state *f;
1449 
	FSM_trans *t;
1450 
 
1451 
	f = fsm_tbl[s];
1452 
	for (t = f->t; t; t = t->nxt)
1453 
	{	if (t->step && t->step->n)
1454 
			switch (t->step->n->ntyp) {
1455 
			case IF:
1456 
			case DO:
1457 
			case ATOMIC:
1458 
			case NON_ATOMIC:
1459 
			case D_STEP:
1460 
				AST_shouldconsider(a, t->to);
1461 
				break;
1462 
			default:
1463 
				AST_track(t->step->n, 0);
1464 
/*
1465 
	AST_track is called here for a blockable stmnt from which
1466 
	a relevant stmnmt was shown to be reachable
1467 
	for a condition this makes all USEs relevant
1468 
	but for a channel operation it only makes the executability
1469 
	relevant -- in those cases, parameters that aren't already
1470 
	relevant may be replaceable with arbitrary tokens
1471 
 */
1472 
				if (AST_suspect(t))
1473 
				{	printf("spin: possibly redundant parameters in: ");
1474 
					comment(stdout, t->step->n, 0);
1475 
					printf("\n");
1476 
				}
1477 
				break;
1478 
			}
1479 
		else	/* an Unless */
1480 
			AST_shouldconsider(a, t->to);
1481 
	}
1482 
}
1483 
 
1484 
static int
1485 
FSM_critical(AST *a, int s)
1486 
{	FSM_state *f;
1487 
	FSM_trans *t;
1488 
 
1489 
	/* is a 1-relevant stmnt reachable from this state? */
1490 
 
1491 
	f = fsm_tbl[s];
1492 
	if (f->seen)
1493 
		goto done;
1494 
	f->seen = 1;
1495 
	f->cr   = 0;
1496 
	for (t = f->t; t; t = t->nxt)
1497 
		if ((t->relevant&1)
1498 
		||  FSM_critical(a, t->to))
1499 
		{	f->cr = 1;
1500 
 
1501 
			if (verbose&32)
1502 
			{	printf("\t\t\t\tcritical(%d) ", t->relevant);
1503 
				comment(stdout, t->step->n, 0);
1504 
				printf("\n");
1505 
			}
1506 
			break;
1507 
		}
1508 
#if 0
1509 
	else {
1510 
		if (verbose&32)
1511 
		{ printf("\t\t\t\tnot-crit ");
1512 
		  comment(stdout, t->step->n, 0);
1513 
	 	  printf("\n");
1514 
		}
1515 
	}
1516 
#endif
1517 
done:
1518 
	return f->cr;
1519 
}
1520 
 
1521 
static void
1522 
AST_ctrl(AST *a)
1523 
{	FSM_state *f;
1524 
	FSM_trans *t;
1525 
	int hit;
1526 
 
1527 
	/* add all blockable transitions
1528 
	 * from which relevant transitions can be reached
1529 
	 */
1530 
	if (verbose&32)
1531 
		printf("CTL -- %s\n", a->p->n->name);
1532 
 
1533 
	/* 1 : mark all blockable edges */
1534 
	for (f = a->fsm; f; f = f->nxt)
1535 
	{	if (!(f->scratch&2))		/* not part of irrelevant subgraph */
1536 
		for (t = f->t; t; t = t->nxt)
1537 
		{	if (t->step && t->step->n)
1538 
			switch (t->step->n->ntyp) {
1539 
			case 'r':
1540 
			case 's':
1541 
			case 'c':
1542 
			case ELSE:
1543 
				t->round = AST_Round;
1544 
				t->relevant |= 2;	/* mark for next phases */
1545 
				if (verbose&32)
1546 
				{	printf("\tpremark ");
1547 
					comment(stdout, t->step->n, 0);
1548 
					printf("\n");
1549 
				}
1550 
				break;
1551 
			default:
1552 
				break;
1553 
	}	}	}
1554 
 
1555 
	/* 2: keep only 2-marked stmnts from which 1-marked stmnts can be reached */
1556 
	for (f = a->fsm; f; f = f->nxt)
1557 
	{	fsm_tbl[f->from] = f;
1558 
		f->seen = 0;	/* used in dfs from FSM_critical */
1559 
	}
1560 
	for (f = a->fsm; f; f = f->nxt)
1561 
	{	if (!FSM_critical(a, f->from))
1562 
		for (t = f->t; t; t = t->nxt)
1563 
			if (t->relevant&2)
1564 
			{	t->relevant &= ~2;	/* clear mark */
1565 
				if (verbose&32)
1566 
				{	printf("\t\tnomark ");
1567 
					if (t->step && t->step->n)
1568 
						comment(stdout, t->step->n, 0);
1569 
					printf("\n");
1570 
	}		}	}
1571 
 
1572 
	/* 3 : lift marks across IF/DO etc. */
1573 
	for (f = a->fsm; f; f = f->nxt)
1574 
	{	hit = 0;
1575 
		for (t = f->t; t; t = t->nxt)
1576 
		{	if (t->step && t->step->n)
1577 
			switch (t->step->n->ntyp) {
1578 
			case IF:
1579 
			case DO:
1580 
			case ATOMIC:
1581 
			case NON_ATOMIC:
1582 
			case D_STEP:
1583 
				if (AST_blockable(a, t->to))
1584 
					hit = 1;
1585 
				break;
1586 
			default:
1587 
				break;
1588 
			}
1589 
			else if (AST_blockable(a, t->to))	/* Unless */
1590 
				hit = 1;
1591 
 
1592 
			if (hit) break;
1593 
		}
1594 
		if (hit)	/* at least one outgoing trans can block */
1595 
		for (t = f->t; t; t = t->nxt)
1596 
		{	t->round = AST_Round;
1597 
			t->relevant |= 2;	/* lift */
1598 
			if (verbose&32)
1599 
			{	printf("\t\t\tliftmark ");
1600 
				if (t->step && t->step->n)
1601 
					comment(stdout, t->step->n, 0);
1602 
				printf("\n");
1603 
			}
1604 
			AST_spread(a, t->to);	/* and spread to all guards */
1605 
	}	}
1606 
 
1607 
	/* 4: nodes with 2-marked out-edges contribute new slice criteria */
1608 
	for (f = a->fsm; f; f = f->nxt)
1609 
	for (t = f->t; t; t = t->nxt)
1610 
		if (t->relevant&2)
1611 
		{	AST_shouldconsider(a, f->from);
1612 
			break;	/* inner loop */
1613 
		}
1614 
}
1615 
 
1616 
static void
1617 
AST_control_dep(void)
1618 
{	AST *a;
1619 
 
1620 
	for (a = ast; a; a = a->nxt)
1621 
	{	if (a->p->b != N_CLAIM && a->p->b != E_TRACE && a->p->b != N_TRACE)
1622 
		{	AST_ctrl(a);
1623 
	}	}
1624 
}
1625 
 
1626 
static void
1627 
AST_prelabel(void)
1628 
{	AST *a;
1629 
	FSM_state *f;
1630 
	FSM_trans *t;
1631 
 
1632 
	for (a = ast; a; a = a->nxt)
1633 
	{	if (a->p->b != N_CLAIM && a->p->b != E_TRACE && a->p->b != N_TRACE)
1634 
		for (f = a->fsm; f; f = f->nxt)
1635 
		for (t = f->t; t; t = t->nxt)
1636 
		{	if (t->step
1637 
			&&  t->step->n
1638 
			&&  t->step->n->ntyp == ASSERT
1639 
			)
1640 
			{	t->relevant |= 1;
1641 
	}	}	}
1642 
}
1643 
 
1644 
static void
1645 
AST_criteria(void)
1646 
{	/*
1647 
	 * remote labels are handled separately -- by making
1648 
	 * sure they are not pruned away during optimization
1649 
	 */
1650 
	AST_Changes = 1;	/* to get started */
1651 
	for (AST_Round = 1; slicer && AST_Changes; AST_Round++)
1652 
	{	AST_Changes = 0;
1653 
		AST_data_dep();
1654 
		AST_preserve();		/* moves processed vars from slicer to rel_vars */
1655 
		AST_dominant();		/* mark data-irrelevant subgraphs */
1656 
		AST_control_dep();	/* can add data deps, which add control deps */
1657 
 
1658 
		if (verbose&32)
1659 
			printf("\n\nROUND %d -- changes %d\n",
1660 
				AST_Round, AST_Changes);
1661 
	}
1662 
}
1663 
 
1664 
static void
1665 
AST_alias_analysis(void)		/* aliasing of promela channels */
1666 
{	AST *a;
1667 
 
1668 
	for (a = ast; a; a = a->nxt)
1669 
		AST_sends(a);		/* collect chan-names that are send across chans */
1670 
 
1671 
	for (a = ast; a; a = a->nxt)
1672 
		AST_para(a->p);		/* aliasing of chans thru proctype parameters */
1673 
 
1674 
	for (a = ast; a; a = a->nxt)
1675 
		AST_other(a);		/* chan params in asgns and recvs */
1676 
 
1677 
	AST_trans();			/* transitive closure of alias table */
1678 
 
1679 
	if (verbose&32)
1680 
		AST_aliases();		/* show channel aliasing info */
1681 
}
1682 
 
1683 
void
1684 
AST_slice(void)
1685 
{	AST *a;
1686 
	int spurious = 0;
1687 
 
1688 
	if (!slicer)
1689 
	{	printf("spin: warning: no slice criteria found (no assertions and no claim)\n");
1690 
		spurious = 1;
1691 
	}
1692 
	AST_dorelevant();		/* mark procs refered to in remote refs */
1693 
 
1694 
	for (a = ast; a; a = a->nxt)
1695 
		AST_def_use(a);		/* compute standard def/use information */
1696 
 
1697 
	AST_hidden();			/* parameter passing and local var inits */
1698 
 
1699 
	AST_alias_analysis();		/* channel alias analysis */
1700 
 
1701 
	AST_prelabel();			/* mark all 'assert(...)' stmnts as relevant */
1702 
	AST_criteria();			/* process the slice criteria from
1703 
					 * asserts and from the never claim
1704 
					 */
1705 
	if (!spurious || (verbose&32))
1706 
	{	spurious = 1;
1707 
		for (a = ast; a; a = a->nxt)
1708 
		{	AST_dump(a);		/* marked up result */
1709 
			if (a->relevant&2)	/* it printed something */
1710 
				spurious = 0;
1711 
		}
1712 
		if (!AST_dump_rel()		/* relevant variables */
1713 
		&&  spurious)
1714 
			printf("spin: no redundancies found (for given property)\n");
1715 
	}
1716 
	AST_suggestions();
1717 
 
1718 
	if (verbose&32)
1719 
		show_expl();
1720 
}
1721 
 
1722 
void
1723 
AST_store(ProcList *p, int start_state)
1724 
{	AST *n_ast;
1725 
 
1726 
	if (p->b != N_CLAIM && p->b != E_TRACE && p->b != N_TRACE)
1727 
	{	n_ast = (AST *) emalloc(sizeof(AST));
1728 
		n_ast->p = p;
1729 
		n_ast->i_st = start_state;
1730 
		n_ast->relevant = 0;
1731 
		n_ast->fsm = fsm;
1732 
		n_ast->nxt = ast;
1733 
		ast = n_ast;
1734 
	}
1735 
	fsm = (FSM_state *) 0;	/* hide it from FSM_DEL */
1736 
}
1737 
 
1738 
static void
1739 
AST_add_explicit(Lextok *d, Lextok *u)
1740 
{	FSM_trans *e = (FSM_trans *) emalloc(sizeof(FSM_trans));
1741 
 
1742 
	e->to = 0;			/* or start_state ? */
1743 
	e->relevant = 0;		/* to be determined */
1744 
	e->step = (Element *) 0;	/* left blank */
1745 
	e->Val[0] = e->Val[1] = (FSM_use *) 0;
1746 
 
1747 
	cur_t = e;
1748 
 
1749 
	def_use(u, USE);
1750 
	def_use(d, DEF);
1751 
 
1752 
	cur_t = (FSM_trans *) 0;
1753 
 
1754 
	e->nxt = explicit;
1755 
	explicit = e;
1756 
}
1757 
 
1758 
static void
1759 
AST_fp1(char *s, Lextok *t, Lextok *f, int parno)
1760 
{	Lextok *v;
1761 
	int cnt;
1762 
 
1763 
	if (!t) return;
1764 
 
1765 
	if (t->ntyp == RUN)
1766 
	{	if (strcmp(t->sym->name, s) == 0)
1767 
		for (v = t->lft, cnt = 1; v; v = v->rgt, cnt++)
1768 
			if (cnt == parno)
1769 
			{	AST_add_explicit(f, v->lft);
1770 
				break;
1771 
			}
1772 
	} else
1773 
	{	AST_fp1(s, t->lft, f, parno);
1774 
		AST_fp1(s, t->rgt, f, parno);
1775 
	}
1776 
}
1777 
 
1778 
static void
1779 
AST_mk1(char *s, Lextok *c, int parno)
1780 
{	AST *a;
1781 
	FSM_state *f;
1782 
	FSM_trans *t;
1783 
 
1784 
	/* concoct an extra FSM_trans *t with the asgn of
1785 
	 * formal par c to matching actual pars made explicit
1786 
	 */
1787 
 
1788 
	for (a = ast; a; a = a->nxt)		/* automata       */
1789 
	for (f = a->fsm; f; f = f->nxt)		/* control states */
1790 
	for (t = f->t; t; t = t->nxt)		/* transitions    */
1791 
	{	if (t->step)
1792 
		AST_fp1(s, t->step->n, c, parno);
1793 
	}
1794 
}
1795 
 
1796 
static void
1797 
AST_par_init(void)	/* parameter passing -- hidden assignments */
1798 
{	AST *a;
1799 
	Lextok *f, *t, *c;
1800 
	int cnt;
1801 
 
1802 
	for (a = ast; a; a = a->nxt)
1803 
	{	if (a->p->b == N_CLAIM || a->p->b == I_PROC
1804 
		||  a->p->b == E_TRACE || a->p->b == N_TRACE)
1805 
		{	continue;			/* has no params */
1806 
		}
1807 
		cnt = 0;
1808 
		for (f = a->p->p; f; f = f->rgt)	/* types */
1809 
		for (t = f->lft; t; t = t->rgt)		/* formals */
1810 
		{	cnt++;				/* formal par count */
1811 
			c = (t->ntyp != ',')? t : t->lft;	/* the formal parameter */
1812 
			AST_mk1(a->p->n->name, c, cnt);		/* all matching run statements */
1813 
	}	}
1814 
}
1815 
 
1816 
static void
1817 
AST_var_init(void)		/* initialized vars (not chans) - hidden assignments */
1818 
{	Ordered	*walk;
1819 
	Lextok *x;
1820 
	Symbol	*sp;
1821 
	AST *a;
1822 
 
1823 
	for (walk = all_names; walk; walk = walk->next)
1824 
	{	sp = walk->entry;
1825 
		if (sp
1826 
		&&  !sp->context		/* globals */
1827 
		&&  sp->type != PROCTYPE
1828 
		&&  sp->ini
1829 
		&& (sp->type != MTYPE || sp->ini->ntyp != CONST) /* not mtype defs */
1830 
		&&  sp->ini->ntyp != CHAN)
1831 
		{	x = nn(ZN, TYPE, ZN, ZN);
1832 
			x->sym = sp;
1833 
			AST_add_explicit(x, sp->ini);
1834 
	}	}
1835 
 
1836 
	for (a = ast; a; a = a->nxt)
1837 
	{	if (a->p->b != N_CLAIM
1838 
		&&  a->p->b != E_TRACE && a->p->b != N_TRACE)	/* has no locals */
1839 
		for (walk = all_names; walk; walk = walk->next)
1840 
		{	sp = walk->entry;
1841 
			if (sp
1842 
			&&  sp->context
1843 
			&&  strcmp(sp->context->name, a->p->n->name) == 0
1844 
			&&  sp->Nid >= 0	/* not a param */
1845 
			&&  sp->type != LABEL
1846 
			&&  sp->ini
1847 
			&&  sp->ini->ntyp != CHAN)
1848 
			{	x = nn(ZN, TYPE, ZN, ZN);
1849 
				x->sym = sp;
1850 
				AST_add_explicit(x, sp->ini);
1851 
	}	}	}
1852 
}
1853 
 
1854 
static void
1855 
show_expl(void)
1856 
{	FSM_trans *t, *T;
1857 
	FSM_use *u;
1858 
 
1859 
	printf("\nExplicit List:\n");
1860 
	for (T = expl_par; T; T = (T == expl_par)?expl_var: (FSM_trans *) 0)
1861 
	{	for (t = T; t; t = t->nxt)
1862 
		{	if (!t->Val[0]) continue;
1863 
			printf("%s", t->relevant?"*":" ");
1864 
			printf("%3d", t->round);
1865 
			for (u = t->Val[0]; u; u = u->nxt)
1866 
			{	printf("\t<");
1867 
				AST_var(u->n, u->n->sym, 1);
1868 
				printf(":%d>, ", u->special);
1869 
			}
1870 
			printf("\n");
1871 
		}
1872 
		printf("==\n");
1873 
	}
1874 
	printf("End\n");
1875 
}
1876 
 
1877 
static void
1878 
AST_hidden(void)			/* reveal all hidden assignments */
1879 
{
1880 
	AST_par_init();
1881 
	expl_par = explicit;
1882 
	explicit = (FSM_trans *) 0;
1883 
 
1884 
	AST_var_init();
1885 
	expl_var = explicit;
1886 
	explicit = (FSM_trans *) 0;
1887 
}
1888 
 
1889 
#define BPW	(8*sizeof(ulong))			/* bits per word */
1890 
 
1891 
static int
1892 
bad_scratch(FSM_state *f, int upto)
1893 
{	FSM_trans *t;
1894 
#if 0
1895 
	1. all internal branch-points have else-s
1896 
	2. all non-branchpoints have non-blocking out-edge
1897 
	3. all internal edges are non-relevant
1898 
	subgraphs like this need NOT contribute control-dependencies
1899 
#endif
1900 
 
1901 
	if (!f->seen
1902 
	||  (f->scratch&4))
1903 
		return 0;
1904 
 
1905 
	if (f->scratch&8)
1906 
		return 1;
1907 
 
1908 
	f->scratch |= 4;
1909 
 
1910 
	if (verbose&32) printf("X[%d:%d:%d] ", f->from, upto, f->scratch);
1911 
 
1912 
	if (f->scratch&1)
1913 
	{	if (verbose&32)
1914 
			printf("\tbad scratch: %d\n", f->from);
1915 
bad:		f->scratch &= ~4;
1916 
	/*	f->scratch |=  8;	 wrong */
1917 
		return 1;
1918 
	}
1919 
 
1920 
	if (f->from != upto)
1921 
	for (t = f->t; t; t = t->nxt)
1922 
		if (bad_scratch(fsm_tbl[t->to], upto))
1923 
			goto bad;
1924 
 
1925 
	return 0;
1926 
}
1927 
 
1928 
static void
1929 
mark_subgraph(FSM_state *f, int upto)
1930 
{	FSM_trans *t;
1931 
 
1932 
	if (f->from == upto
1933 
	||  !f->seen
1934 
	||  (f->scratch&2))
1935 
		return;
1936 
 
1937 
	f->scratch |= 2;
1938 
 
1939 
	for (t = f->t; t; t = t->nxt)
1940 
		mark_subgraph(fsm_tbl[t->to], upto);
1941 
}
1942 
 
1943 
static void
1944 
AST_pair(AST *a, FSM_state *h, int y)
1945 
{	Pair *p;
1946 
 
1947 
	for (p = a->pairs; p; p = p->nxt)
1948 
		if (p->h == h
1949 
		&&  p->b == y)
1950 
			return;
1951 
 
1952 
	p = (Pair *) emalloc(sizeof(Pair));
1953 
	p->h = h;
1954 
	p->b = y;
1955 
	p->nxt = a->pairs;
1956 
	a->pairs = p;
1957 
}
1958 
 
1959 
static void
1960 
AST_checkpairs(AST *a)
1961 
{	Pair *p;
1962 
 
1963 
	for (p = a->pairs; p; p = p->nxt)
1964 
	{	if (verbose&32)
1965 
			printf("	inspect pair %d %d\n", p->b, p->h->from);
1966 
		if (!bad_scratch(p->h, p->b))	/* subgraph is clean */
1967 
		{	if (verbose&32)
1968 
				printf("subgraph: %d .. %d\n", p->b, p->h->from);
1969 
			mark_subgraph(p->h, p->b);
1970 
		}
1971 
	}
1972 
}
1973 
 
1974 
static void
1975 
subgraph(AST *a, FSM_state *f, int out)
1976 
{	FSM_state *h;
1977 
	int i, j;
1978 
	ulong *g;
1979 
#if 0
1980 
	reverse dominance suggests that this is a possible
1981 
	entry and exit node for a proper subgraph
1982 
#endif
1983 
	h = fsm_tbl[out];
1984 
 
1985 
	i = f->from / BPW;
1986 
	j = f->from % BPW;
1987 
	g = h->mod;
1988 
 
1989 
	if (verbose&32)
1990 
		printf("possible pair %d %d -- %d\n",
1991 
			f->from, h->from, (g[i]&(1<<j))?1:0);
1992 
 
1993 
	if (g[i]&(1<<j))		/* also a forward dominance pair */
1994 
		AST_pair(a, h, f->from);	/* record this pair */
1995 
}
1996 
 
1997 
static void
1998 
act_dom(AST *a)
1999 
{	FSM_state *f;
2000 
	FSM_trans *t;
2001 
	int i, j, cnt;
2002 
 
2003 
	for (f = a->fsm; f; f = f->nxt)
2004 
	{	if (!f->seen) continue;
2005 
#if 0
2006 
		f->from is the exit-node of a proper subgraph, with
2007 
		the dominator its entry-node, if:
2008 
		a. this node has more than 1 reachable predecessor
2009 
		b. the dominator has more than 1 reachable successor
2010 
		   (need reachability - in case of reverse dominance)
2011 
		d. the dominator is reachable, and not equal to this node
2012 
#endif
2013 
		for (t = f->p, i = 0; t; t = t->nxt)
2014 
			i += fsm_tbl[t->to]->seen;
2015 
		if (i <= 1) continue;					/* a. */
2016 
 
2017 
		for (cnt = 1; cnt < a->nstates; cnt++)	/* 0 is endstate */
2018 
		{	if (cnt == f->from
2019 
			||  !fsm_tbl[cnt]->seen)
2020 
				continue;				/* c. */
2021 
 
2022 
			i = cnt / BPW;
2023 
			j = cnt % BPW;
2024 
			if (!(f->dom[i]&(1<<j)))
2025 
				continue;
2026 
 
2027 
			for (t = fsm_tbl[cnt]->t, i = 0; t; t = t->nxt)
2028 
				i += fsm_tbl[t->to]->seen;
2029 
			if (i <= 1)
2030 
				continue;				/* b. */
2031 
 
2032 
			if (f->mod)			/* final check in 2nd phase */
2033 
				subgraph(a, f, cnt);	/* possible entry-exit pair */
2034 
		}
2035 
	}
2036 
}
2037 
 
2038 
static void
2039 
reachability(AST *a)
2040 
{	FSM_state *f;
2041 
 
2042 
	for (f = a->fsm; f; f = f->nxt)
2043 
		f->seen = 0;		/* clear */
2044 
	AST_dfs(a, a->i_st, 0);		/* mark 'seen' */
2045 
}
2046 
 
2047 
static int
2048 
see_else(FSM_state *f)
2049 
{	FSM_trans *t;
2050 
 
2051 
	for (t = f->t; t; t = t->nxt)
2052 
	{	if (t->step
2053 
		&&  t->step->n)
2054 
		switch (t->step->n->ntyp) {
2055 
		case ELSE:
2056 
			return 1;
2057 
		case IF:
2058 
		case DO:
2059 
		case ATOMIC:
2060 
		case NON_ATOMIC:
2061 
		case D_STEP:
2062 
			if (see_else(fsm_tbl[t->to]))
2063 
				return 1;
2064 
		default:
2065 
			break;
2066 
		}
2067 
	}
2068 
	return 0;
2069 
}
2070 
 
2071 
static int
2072 
is_guard(FSM_state *f)
2073 
{	FSM_state *g;
2074 
	FSM_trans *t;
2075 
 
2076 
	for (t = f->p; t; t = t->nxt)
2077 
	{	g = fsm_tbl[t->to];
2078 
		if (!g->seen)
2079 
			continue;
2080 
 
2081 
		if (t->step
2082 
		&&  t->step->n)
2083 
		switch(t->step->n->ntyp) {
2084 
		case IF:
2085 
		case DO:
2086 
			return 1;
2087 
		case ATOMIC:
2088 
		case NON_ATOMIC:
2089 
		case D_STEP:
2090 
			if (is_guard(g))
2091 
				return 1;
2092 
		default:
2093 
			break;
2094 
		}
2095 
	}
2096 
	return 0;
2097 
}
2098 
 
2099 
static void
2100 
curtail(AST *a)
2101 
{	FSM_state *f, *g;
2102 
	FSM_trans *t;
2103 
	int i, haselse, isrel, blocking;
2104 
#if 0
2105 
	mark nodes that do not satisfy these requirements:
2106 
	1. all internal branch-points have else-s
2107 
	2. all non-branchpoints have non-blocking out-edge
2108 
	3. all internal edges are non-data-relevant
2109 
#endif
2110 
	if (verbose&32)
2111 
		printf("Curtail %s:\n", a->p->n->name);
2112 
 
2113 
	for (f = a->fsm; f; f = f->nxt)
2114 
	{	if (!f->seen
2115 
		||  (f->scratch&(1|2)))
2116 
			continue;
2117 
 
2118 
		isrel = haselse = i = blocking = 0;
2119 
 
2120 
		for (t = f->t; t; t = t->nxt)
2121 
		{	g = fsm_tbl[t->to];
2122 
 
2123 
			isrel |= (t->relevant&1);	/* data relevant */
2124 
			i += g->seen;
2125 
 
2126 
			if (t->step
2127 
			&&  t->step->n)
2128 
			{	switch (t->step->n->ntyp) {
2129 
				case IF:
2130 
				case DO:
2131 
					haselse |= see_else(g);
2132 
					break;
2133 
				case 'c':
2134 
				case 's':
2135 
				case 'r':
2136 
					blocking = 1;
2137 
					break;
2138 
		}	}	}
2139 
#if 0
2140 
		if (verbose&32)
2141 
			printf("prescratch %d -- %d %d %d %d -- %d\n",
2142 
				f->from, i, isrel, blocking, haselse, is_guard(f));
2143 
#endif
2144 
		if (isrel			/* 3. */
2145 
		||  (i == 1 && blocking)	/* 2. */
2146 
		||  (i >  1 && !haselse))	/* 1. */
2147 
		{	if (!is_guard(f))
2148 
			{	f->scratch |= 1;
2149 
				if (verbose&32)
2150 
				printf("scratch %d -- %d %d %d %d\n",
2151 
					f->from, i, isrel, blocking, haselse);
2152 
			}
2153 
		}
2154 
	}
2155 
}
2156 
 
2157 
static void
2158 
init_dom(AST *a)
2159 
{	FSM_state *f;
2160 
	int i, j, cnt;
2161 
#if 0
2162 
	(1)  D(s0) = {s0}
2163 
	(2)  for s in S - {s0} do D(s) = S
2164 
#endif
2165 
 
2166 
	for (f = a->fsm; f; f = f->nxt)
2167 
	{	if (!f->seen) continue;
2168 
 
2169 
		f->dom = (ulong *)
2170 
			emalloc(a->nwords * sizeof(ulong));
2171 
 
2172 
		if (f->from == a->i_st)
2173 
		{	i = a->i_st / BPW;
2174 
			j = a->i_st % BPW;
2175 
			f->dom[i] = (1<<j);			/* (1) */
2176 
		} else						/* (2) */
2177 
		{	for (i = 0; i < a->nwords; i++)
2178 
				f->dom[i] = (ulong) ~0;			/* all 1's */
2179 
 
2180 
			if (a->nstates % BPW)
2181 
			for (i = (a->nstates % BPW); i < (int) BPW; i++)
2182 
				f->dom[a->nwords-1] &= ~(1<<i);	/* clear tail */
2183 
 
2184 
			for (cnt = 0; cnt < a->nstates; cnt++)
2185 
				if (!fsm_tbl[cnt]->seen)
2186 
				{	i = cnt / BPW;
2187 
					j = cnt % BPW;
2188 
					f->dom[i] &= ~(1<<j);
2189 
	}	}		}
2190 
}
2191 
 
2192 
static int
2193 
dom_perculate(AST *a, FSM_state *f)
2194 
{	static ulong *ndom = (ulong *) 0;
2195 
	static int on = 0;
2196 
	int i, j, cnt = 0;
2197 
	FSM_state *g;
2198 
	FSM_trans *t;
2199 
 
2200 
	if (on < a->nwords)
2201 
	{	on = a->nwords;
2202 
		ndom = (ulong *)
2203 
			emalloc(on * sizeof(ulong));
2204 
	}
2205 
 
2206 
	for (i = 0; i < a->nwords; i++)
2207 
		ndom[i] = (ulong) ~0;
2208 
 
2209 
	for (t = f->p; t; t = t->nxt)	/* all reachable predecessors */
2210 
	{	g = fsm_tbl[t->to];
2211 
		if (g->seen)
2212 
		for (i = 0; i < a->nwords; i++)
2213 
			ndom[i] &= g->dom[i];	/* (5b) */
2214 
	}
2215 
 
2216 
	i = f->from / BPW;
2217 
	j = f->from % BPW;
2218 
	ndom[i] |= (1<<j);			/* (5a) */
2219 
 
2220 
	for (i = 0; i < a->nwords; i++)
2221 
		if (f->dom[i] != ndom[i])
2222 
		{	cnt++;
2223 
			f->dom[i] = ndom[i];
2224 
		}
2225 
 
2226 
	return cnt;
2227 
}
2228 
 
2229 
static void
2230 
dom_forward(AST *a)
2231 
{	FSM_state *f;
2232 
	int cnt;
2233 
 
2234 
	init_dom(a);						/* (1,2) */
2235 
	do {
2236 
		cnt = 0;
2237 
		for (f = a->fsm; f; f = f->nxt)
2238 
		{	if (f->seen
2239 
			&&  f->from != a->i_st)			/* (4) */
2240 
				cnt += dom_perculate(a, f);	/* (5) */
2241 
		}
2242 
	} while (cnt);						/* (3) */
2243 
	dom_perculate(a, fsm_tbl[a->i_st]);
2244 
}
2245 
 
2246 
static void
2247 
AST_dominant(void)
2248 
{	FSM_state *f;
2249 
	FSM_trans *t;
2250 
	AST *a;
2251 
	int oi;
2252 
	static FSM_state no_state;
2253 
#if 0
2254 
	find dominators
2255 
	Aho, Sethi, & Ullman, Compilers - principles, techniques, and tools
2256 
	Addison-Wesley, 1986, p.671.
2257 
 
2258 
	(1)  D(s0) = {s0}
2259 
	(2)  for s in S - {s0} do D(s) = S
2260 
 
2261 
	(3)  while any D(s) changes do
2262 
	(4)    for s in S - {s0} do
2263 
	(5)	D(s) = {s} union  with intersection of all D(p)
2264 
		where p are the immediate predecessors of s
2265 
 
2266 
	the purpose is to find proper subgraphs
2267 
	(one entry node, one exit node)
2268 
#endif
2269 
	if (AST_Round == 1)	/* computed once, reused in every round */
2270 
	for (a = ast; a; a = a->nxt)
2271 
	{	a->nstates = 0;
2272 
		for (f = a->fsm; f; f = f->nxt)
2273 
		{	a->nstates++;				/* count */
2274 
			fsm_tbl[f->from] = f;			/* fast lookup */
2275 
			f->scratch = 0;				/* clear scratch marks */
2276 
		}
2277 
		for (oi = 0; oi < a->nstates; oi++)
2278 
			if (!fsm_tbl[oi])
2279 
				fsm_tbl[oi] = &no_state;
2280 
 
2281 
		a->nwords = (a->nstates + BPW - 1) / BPW;	/* round up */
2282 
 
2283 
		if (verbose&32)
2284 
		{	printf("%s (%d): ", a->p->n->name, a->i_st);
2285 
			printf("states=%d (max %d), words = %d, bpw %d, overflow %d\n",
2286 
				a->nstates, o_max, a->nwords,
2287 
				(int) BPW, (int) (a->nstates % BPW));
2288 
		}
2289 
 
2290 
		reachability(a);
2291 
		dom_forward(a);		/* forward dominance relation */
2292 
 
2293 
		curtail(a);		/* mark ineligible edges */
2294 
		for (f = a->fsm; f; f = f->nxt)
2295 
		{	t = f->p;
2296 
			f->p = f->t;
2297 
			f->t = t;	/* invert edges */
2298 
 
2299 
			f->mod = f->dom;
2300 
			f->dom = (ulong *) 0;
2301 
		}
2302 
		oi = a->i_st;
2303 
		if (fsm_tbl[0]->seen)	/* end-state reachable - else leave it */
2304 
			a->i_st = 0;	/* becomes initial state */
2305 
 
2306 
		dom_forward(a);		/* reverse dominance -- don't redo reachability! */
2307 
		act_dom(a);		/* mark proper subgraphs, if any */
2308 
		AST_checkpairs(a);	/* selectively place 2 scratch-marks */
2309 
 
2310 
		for (f = a->fsm; f; f = f->nxt)
2311 
		{	t = f->p;
2312 
			f->p = f->t;
2313 
			f->t = t;	/* restore */
2314 
		}
2315 
		a->i_st = oi;	/* restore */
2316 
	} else
2317 
		for (a = ast; a; a = a->nxt)
2318 
		{	for (f = a->fsm; f; f = f->nxt)
2319 
			{	fsm_tbl[f->from] = f;
2320 
				f->scratch &= 1; /* preserve 1-marks */
2321 
			}
2322 
			for (oi = 0; oi < a->nstates; oi++)
2323 
				if (!fsm_tbl[oi])
2324 
					fsm_tbl[oi] = &no_state;
2325 
 
2326 
			curtail(a);		/* mark ineligible edges */
2327 
 
2328 
			for (f = a->fsm; f; f = f->nxt)
2329 
			{	t = f->p;
2330 
				f->p = f->t;
2331 
				f->t = t;	/* invert edges */
2332 
			}
2333 
 
2334 
			AST_checkpairs(a);	/* recompute 2-marks */
2335 
 
2336 
			for (f = a->fsm; f; f = f->nxt)
2337 
			{	t = f->p;
2338 
				f->p = f->t;
2339 
				f->t = t;	/* restore */
2340 
		}	}
2341 
}