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