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