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