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