sys/src/cmd/spin/pangen6.c

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