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