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