sys/src/cmd/spin/pangen6.c

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